Theorems · Theorem · group theory
AddEquiv.coe_addMonoidHom_symm_comp_coe_addMonoidHom
∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (e : M ≃+ N),
(↑e.symm).comp ↑e = AddMonoidHom.id M- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Quot.sound
- Assumes
- AddZeroClassAddZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidHomstatement · cited by 3,230
- AddZeroClassstatement and proof · cited by 1,237
- AddEquivstatement and proof · cited by 1,087
- AddEquiv.symmstatement · cited by 530
- AddMonoidHom.compstatement · cited by 339
- AddMonoidHomClass.toAddMonoidHomstatement · cited by 232
- AddMonoidHom.extproof · cited by 149
- AddMonoidHom.idstatement · cited by 107
- AddMonoidHom.id_applyproof · cited by 29
- AddEquiv.symm_apply_applyproof · cited by 19
Cited by1
Results whose statement or proof uses this declaration.
- AddEquiv.comp_right_injectiveproof · cited by 0