Theorems · Definition · commutative algebra

IsLocalization.commonDenom

{R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      {S : Type u_2} →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] → [IsLocalization M S] → {ι : Type u_4} → Finset ι → (ι → S) → ↥M

A choice of a common multiple of the denominators of a Finset-indexed family of fractions.

Defined in: Mathlib.RingTheory.Localization.Integer
Cited by: 4 results in Mathlib
Foundations: Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring CommSemiring Algebra IsLocalization

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Finsetstatement and proof · cited by 13,712
Algebrastatement and proof · cited by 11,388
CommSemiringstatement and proof · cited by 10,911
Submonoidstatement and proof · cited by 3,086
IsLocalizationstatement and proof · cited by 636
IsLocalization.exist_integer_multiplesproof · cited by 4

Cited by5

Results whose statement or proof uses this declaration.

IsIntegral.exists_multiple_integral_of_isLocalizationproof · cited by 7
IsLocalization.commonDenomOfFinsetproof · cited by 4
IsLocalization.map_integerMultiplestatement · cited by 3
IsLocalization.integerMultiple_injectiveproof · cited by 2
IsLocalization.scaleRoots_commonDenom_mem_liftsstatement and proof · cited by 1