Theorems · Definition · group theory
MulAut
(M : Type u_7) → [Mul M] → Type u_7
The group of multiplicative automorphisms.
- Defined in
- Mathlib.Algebra.Group.End
- Cited by
- 158 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 3 definitions · uses no axioms
- Assumes
- Mul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MulEquivproof · cited by 1,142
Cited by200
Results whose statement or proof uses this declaration.
- SemidirectProductstatement · cited by 69
- MulAut.conjstatement · cited by 64
- SemidirectProduct.rightstatement and proof · cited by 35
- SemidirectProduct.leftstatement and proof · cited by 30
- SemidirectProduct.inlstatement and proof · cited by 20
- SemidirectProduct.inrstatement and proof · cited by 18
- Subgroup.normalizerMonoidHomstatement · cited by 10
- MulAut.conjNormalstatement · cited by 9
- SemidirectProduct.rightHomstatement and proof · cited by 9
- MulAut.inv_applystatement and proof · cited by 8
- SemidirectProduct.mapstatement and proof · cited by 8
- SemidirectProduct.extstatement and proof · cited by 7