Theorems · Definition · group theory
invMonoidHom
{α : Type u_1} → [inst : DivisionCommMonoid α] → α →* αInversion on a commutative group, considered as a monoid homomorphism.
- Defined in
- Mathlib.Algebra.Group.Hom.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext
- Assumes
- DivisionCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MonoidHomstatement · cited by 3,629
- DivisionCommMonoidstatement and proof · cited by 80
- mul_invproof · cited by 50
Cited by9
Results whose statement or proof uses this declaration.
- coe_invMonoidHomstatement · cited by 1
- Multiset.prod_map_inv'proof · cited by 1
- IsMulIndecomposable.image_baseOf_inv_comp_eqstatement and proof · cited by 1
- invMonoidHom_comp_invMonoidHomstatement · cited by 1
- ContinuousMonoidHom.invproof · cited by 1
- Subgroup.closure_image_isMulIndecomposable_baseOfproof · cited by 0
- invMonoidWithZeroHomproof · cited by 0
- invMonoidHom_applystatement · cited by 0
- DFinsupp.prod_invproof · cited by 0