Theorems · Inductive type · group theory
MulEquivClass
(F : Type u_9) → (A : outParam (Type u_10)) → (B : outParam (Type u_11)) → [Mul A] → [Mul B] → [EquivLike F A B] → Prop
MulEquivClass F A B states that F is a type of multiplication-preserving morphisms.
You should extend this class when you extend MulEquiv.
- Defined in
- Mathlib.Algebra.Group.Equiv.Defs
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
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.
- EquivLikestatement · cited by 165
Cited by41
Results whose statement or proof uses this declaration.
- MulEquivClass.toMulEquivstatement and proof · cited by 57
- map_dvd_iffstatement and proof · cited by 3
- MulEquivClass.coe_symm_apply_applystatement and proof · cited by 3
- MulEquiv.irreducible_iffstatement and proof · cited by 3
- emultiplicity_map_eqstatement and proof · cited by 2
- StarMulEquiv.ofClassstatement and proof · cited by 2
- UniqueFactorizationMonoid.normalizedFactorsEquivstatement and proof · cited by 2
- MulEquivClass.apply_mem_center_iffstatement and proof · cited by 2
- MulEquivClass.map_nonZeroDivisorsstatement and proof · cited by 2
- Submonoid.map_coe_toMulEquivstatement and proof · cited by 1
- Irreducible.mapstatement and proof · cited by 1
- multiplicity_map_eqstatement and proof · cited by 1