Theorems · Definition · ring theory
OreLocalization.numeratorHom
{R : Type u_1} → [inst : Monoid R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → R →* OreLocalization S RThe multiplicative homomorphism from R to R[S⁻¹], mapping r : R to the
fraction r /ₒ 1.
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 36 from the axioms · uses propext, Quot.sound
- Assumes
- MonoidOreLocalization.OreSet
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.
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement · cited by 3,629
- Submonoidstatement and proof · cited by 3,086
- OreLocalization.OreSetstatement and proof · cited by 92
- OreLocalizationstatement · cited by 90
- OreLocalization.oreDivproof · cited by 72
Cited by9
Results whose statement or proof uses this declaration.
- OreLocalization.numeratorHom_applystatement · cited by 2
- OreLocalization.numeratorRingHomproof · cited by 2
- OreLocalization.numeratorHom_injstatement and proof · cited by 1
- OreLocalization.universalMulHom_uniquestatement and proof · cited by 1
- OreLocalization.universalHom_commutesstatement · cited by 0
- OreLocalization.universalHom_uniquestatement and proof · cited by 0
- OreLocalization.numeratorHom_surjective_of_finitestatement · cited by 0
- OreLocalization.universalMulHom_commutesstatement · cited by 0
- OreLocalization.numerator_isUnitstatement · cited by 0