Integer elements of a localized module #
This is a mirror of the corresponding notion for localizations of rings.
Main definitions #
IsLocalizedModule.IsInteger
is a predicate stating thatm : M'
is in the image ofM
Implementation details #
After IsLocalizedModule
and IsLocalization
are unified, the two IsInteger
predicates
can be unified.
Given x : M'
, M'
a localization of M
via f
, IsInteger f x
iff x
is in the image of
the localization map f
.
Instances For
Each element x : M'
has an S
-multiple which is an integer.
We can clear the denominators of a Finset
-indexed family of fractions.
We can clear the denominators of a finite indexed family of fractions.
We can clear the denominators of a finite set of fractions.
A choice of a common multiple of the denominators of a Finset
-indexed family of fractions.
Instances For
The numerator of a fraction after clearing the denominators
of a Finset
-indexed family of fractions.
Instances For
A choice of a common multiple of the denominators of a finite set of fractions.
Instances For
The finset of numerators after clearing the denominators of a finite set of fractions.