Structures · Algebra
MulEquivClass
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
- Shape
- 3 explicit arguments · adds map_mul
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances5
- MulEquiv
- OrderMonoidIso
- ContinuousMulEquiv
- StarMulEquiv
- GroupExtension.Equiv
How is a type an instance?
Loading the hierarchy index…
Assumed by42
- MulEquivClass.toMulEquiv
- MulEquivClass.coe_symm_apply_apply
- map_dvd_iff
- MulEquiv.irreducible_iff
- StarMulEquiv.ofClass
- MulEquivClass.apply_mem_center_iff
- MulEquivClass.map_nonZeroDivisors
- emultiplicity_map_eq
- UniqueFactorizationMonoid.normalizedFactorsEquiv
- MulEquivClass.toMulEquiv.congr_simp
- MulEquiv.prime_iff
- Subgroup.map_equiv_top
- Submonoid.map_coe_toMulEquiv
- MulEquivClass.map_finprod
- map_finsetProd
- MulEquivClass.apply_coe_symm_apply
- multiplicity_map_eq
- MulEquivClass.isDedekindFiniteMonoid_iff
- MulEquivClass.apply_mem_center
- Irreducible.map
- MulEquivClass.map_mul
- UniqueFactorizationMonoid.normalizedFactorsEquiv_apply
- MulEquivClass.toMulEquiv_injective
- MulEquivClass.toZeroHomClass
- OrderMonoidIsoClass.toOrderMonoidIso
- StarMulEquiv.ofClass_apply
- isLocalHom_equiv
- MulEquivClass.isMulFreimanIso
- map_dvd_iff_dvd_symm
- Submonoid.IsLocalizationMap.mulEquiv_comp
- MulEquivClass.toMonoidWithZeroHomClass
- MulEquivClass.instMonoidHomClass
- MulEquiv.decompositionMonoid
- UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply
- Multipliable.map_iff_of_equiv
- instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass
- map_finset_prod
- MulEquiv.isUnit_map
- MulEquiv.toRingEquiv
- instCoeTCMulEquivOfMulEquivClass
- MulEquivClass.instMulHomClass
- StarMulEquiv.ofClass_symm_apply
Ancestors0
No ancestors.