Structures · Algebra
IsMulCommutative
A Prop stating that the multiplication is commutative.
- Defined in
- Mathlib.Algebra.Group.Defs
- Shape
- One type argument · adds is_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances4
- CategoryTheory.CatCenter
- Subtype
- Prod
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by91
- mul_comm'
- setLike_mul_comm
- posMulStrictMono_iff_mulPosStrictMono
- posMulMono_iff_mulPosMono
- Subgroup.le_centralizer
- Subgroup.QuotientDiff
- NonUnitalSubsemiring.isMulCommutative_iSup
- Subgroup.smul_diff'
- Subsemigroup.isMulCommutative_iSup
- MulLECancellable.injective_left
- Subgroup.exists_smul_eq
- posMulReflectLE_iff_mulPosReflectLE
- Sylow.conj_eq_normalizer_conj_of_mem
- Subsemiring.isMulCommutative_iSup
- posMulReflectLT_iff_mulPosReflectLT
- Subalgebra.isMulCommutative_iSup
- IsCyclotomicExtension.Rat.card_subgroupGalEquivSubgroupChar
- Subgroup.eq_one_of_smul_eq_one
- Subgroup.center_eq_top
- IsSimpleModule.finrank_eq_one_of_isMulCommutative
- Group.is_simple_iff_prime_card
- Subgroup.instInhabitedQuotientDiff
- IsMulCommutative.instNonAssocCommSemiring
- Subgroup.instIsMulCommutativeSubtypeMem
- IsMulCommutative.instNonUnitalCommSemiring
- Subgroup.comap_injective_isMulCommutative
- Pi.isMulCommutative
- Subalgebra.instIsMulCommutative_iSup
- NonUnitalSubsemiring.instIsMulCommutative_iSup
- Subgroup.isComplement'_stabilizer_of_coprime
- Subgroup.normal_of_comm
- Prod.isMulCommutative
- IsMulCommutative.instNonUnitalNonAssocCommSemiring
- MulLECancellable.mul_le_iff_le_one_left
- Algebra.instIsMulCommutative_adjoin
- IsMulCommutative.is_comm
- IsMulCommutative.instCommRing
- Subgroup.instIsMulCommutative_iSup
- IsMulCommutative.instNonUnitalCommRing
- IsMulCommutative.instNonUnitalNonAssocCommRing
- PosMulMono.toMulPosMono
- Subsemiring.instIsMulCommutative_closure
- NonUnitalStarAlgebra.instIsMulCommutative_adjoin
- PosMulStrictMono.toMulPosStrictMono
- NonUnitalStarSubalgebra.isMulCommutative_iSup
- Submonoid.instIsMulCommutative_iSup
- StarSubalgebra.instIsMulCommutative_iSup
- NonUnitalSubalgebra.instIsMulCommutative_iSup
- Submonoid.instIsMulCommutative_closure
- IsMulCommutative.instCommMagma
Ancestors0
No ancestors.