Theorems · Definition · group theory
MulEquiv.inv
(G : Type u_6) → [inst : DivisionCommMonoid G] → G ≃* G
In a DivisionCommMonoid, Equiv.inv is a MulEquiv. There is a variant of this
MulEquiv.inv' G : G ≃* Gᵐᵒᵖ for the non-commutative case.
- Defined in
- Mathlib.Algebra.Group.Units.Equiv
- Cited by
- 5 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.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Equiv.Permproof · cited by 1,375
- MulEquivstatement · cited by 1,142
- DivisionCommMonoidstatement and proof · cited by 80
- Equiv.right_invproof · cited by 68
- Equiv.left_invproof · cited by 59
- mul_invproof · cited by 50
- Equiv.invproof · cited by 23
Cited by5
Results whose statement or proof uses this declaration.
- finprod_inv_distribproof · cited by 2
- mulDissociated_invproof · cited by 2
- finprod_mem_inv_distribproof · cited by 1
- MulEquiv.inv_applystatement and proof · cited by 0
- MulEquiv.inv_symmstatement · cited by 0