Theorems · Definition · ring theory
RingEquiv.toNonUnitalRingHom
{R : Type u_4} →
{S : Type u_5} → [inst : NonUnitalNonAssocSemiring R] → [inst_1 : NonUnitalNonAssocSemiring S] → R ≃+* S → R →ₙ+* SReinterpret a ring equivalence as a non-unital ring homomorphism.
- Defined in
- Mathlib.Algebra.Ring.Equiv
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidHomproof · cited by 3,230
- RingEquivstatement and proof · cited by 1,147
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- MulHomproof · cited by 299
- NonUnitalRingHomstatement · cited by 157
- AddEquiv.toAddMonoidHomproof · cited by 101
- RingEquiv.toMulEquivproof · cited by 26
- RingEquiv.toAddEquivproof · cited by 13
- MulEquiv.toMulHomproof · cited by 9
Cited by13
Results whose statement or proof uses this declaration.
- RingEquiv.nonUnitalSubsemiringMapstatement · cited by 2
- RingEquiv.symm_toNonUnitalRingHom_comp_toNonUnitalRingHomstatement · cited by 1
- RingEquiv.toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_applystatement · cited by 0
- RingEquiv.toNonUnitalRingHom_eq_coestatement · cited by 0
- RingEquiv.toNonUnitalRingHom_injectivestatement and proof · cited by 0
- RingEquiv.toNonUnitalRingHom_reflstatement · cited by 0
- RingEquiv.toNonUnitalRingHom_transstatement · cited by 0
- RingEquiv.toNonUnitalRingHomm_comp_symm_toNonUnitalRingHomstatement · cited by 0
- RingCon.comap_ringConGen_ringEquivproof · cited by 0
- RingEquiv.nonUnitalSubsemiringMap_apply_coestatement · cited by 0
- RingEquiv.nonUnitalSubsemiringMap_symm_apply_coestatement · cited by 0
- RingEquiv.coe_toNonUnitalRingHom'statement · cited by 0