Structures · Algebra
IsAddCommutative
A Prop stating that the addition 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 by0
Nothing extends this class yet.
Concrete types that are instances4
- Matrix
- Subtype
- Prod
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by37
- add_comm'
- AddLECancellable.inj_left
- setLike_add_comm
- AddLECancellable.add_le_add_iff_right
- AddLECancellable.add_le_iff_nonpos_left
- AddLECancellable.injective_left
- AddGroup.is_simple_iff_prime_card
- IsAddCommutative.instAddCommSemigroup
- AddSubsemigroup.instIsAddCommutative_closure
- AddSubsemigroup.isAddCommutative_iSup
- AddSubgroup.addSubgroupOf_isAddCommutative
- AddLECancellable.le_add_iff_nonneg_left
- AddSubgroup.comap_injective_isAddCommutative
- AddSubgroup.instIsAddCommutative_iSup
- AddSubgroup.map_isAddCommutative
- AddSubgroup.instIsAddCommutativeSubtypeMem
- AddSubgroup.center_eq_top
- AddSubgroup.normal_of_isAddCommutative
- AddSubgroup.range_isAddCommutative
- Pi.isAddCommutative
- AddSubgroup.add_comm_of_mem_isAddCommutative
- IsAddCommutative.is_comm
- AddSubgroup.instIsAddCommutative_closure
- AddSubsemigroup.instIsAddCommutative_iSup
- AddSubmonoid.instIsAddCommutative_iSup
- AddSubmonoid.instIsAddCommutative_closure
- AddSubmonoid.isAddCommutative_iSup
- IsAddCommutative.instDivisionAddCommMonoid
- IsAddCommutative.instAddCommMagma
- Prod.isAddCommutative
- Matrix.instIsAddCommutative
- addCommutator_eq_bot
- AddSubgroup.isAddCommutative_iSup
- AddSubgroup.le_centralizer
- instIsDedekindFiniteAddMonoidOfIsAddCommutative
- IsAddCommutative.instAddCommMonoid
- IsAddCommutative.instAddCommGroup
Ancestors0
No ancestors.