Theorems · Definition · ring theory
RingEquiv.toMonoidHom
{R : Type u_4} → {S : Type u_5} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R ≃+* S → R →* SReinterpret a ring equivalence as a monoid homomorphism.
- Defined in
- Mathlib.Algebra.Ring.Equiv
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MonoidHomstatement · cited by 3,629
- RingEquivstatement and proof · cited by 1,147
- NonAssocSemiringstatement and proof · cited by 805
- RingEquiv.toRingHomproof · cited by 150
- RingHom.toMonoidHomproof · cited by 132
Cited by21
Results whose statement or proof uses this declaration.
- FDRep.ρproof · cited by 20
- IsLocalization.ringEquivOfRingEquivstatement and proof · cited by 15
- FDRep.ofproof · cited by 8
- IsLocalization.ringEquivOfRingEquiv_applystatement and proof · cited by 5
- Rep.RepToActionproof · cited by 4
- Rep.ActionToRepproof · cited by 3
- Algebra.IsStandardEtale.of_isLocalizationAwayproof · cited by 2
- LocallyConstant.congrRightRingEquivproof · cited by 2
- FDRep.of_ρstatement · cited by 0
- Rep.ActionToRep_mapstatement · cited by 0
- Rep.ActionToRep_obj_ρstatement · cited by 0
- RingEquiv.toMonoidHom_reflstatement · cited by 0