Structures · Algebra
VAddCommClass
A typeclass mixin saying that two additive actions on the same space commute.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Shape
- 3 explicit arguments · adds vadd_comm
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances11
- DomAddAct
- AddUnits
- Subtype
- OrderDual
- PUnit
- Lex
- AddOpposite
- Additive
- Set
- Finset
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by103
- VAddCommClass.vadd_comm
- add_vadd_comm
- AddSemiconjBy.vadd_right
- vadd_vadd_vadd_comm
- AddSemiconjBy.vadd_left
- vadd_add_vadd_comm
- AddSemiconjBy.vadd_right_iff
- MeasureTheory.IsAddFundamentalDomain.vadd_of_comm
- VAddCommClass.symm
- vadd_add_vadd
- AddAction.stabilizer_vadd_eq_right
- List.vadd_sum
- AddUnits.val_vadd
- AddSemiconjBy.vadd_left_iff
- VAddCommClass.toAddActionHom
- AddAction.le_stabilizer_vadd_right
- VAdd.comp.vaddCommClass
- AddUnits.vaddCommClass_left
- SeparationQuotient.instVAddCommClass
- AddCommute.vadd_left
- DomAddAct.instVAddCommClassAEEqFun_2
- AddSubgroup.vaddCommClass_left
- VAddAssocClass.opposite_mid
- Filter.vaddCommClass_filter''
- Sum.instVAddCommClass
- OrderDual.instVAddCommClass
- AddUnits.vadd_neg
- AddSubmonoid.vaddCommClass_right
- Function.vaddCommClass
- OrderDual.instVAddCommClass_1
- Option.instVAddCommClass
- AddUnits.vaddCommClass'
- OrderDual.instVAddCommClass_2
- Prod.vaddCommClassBoth
- add_vadd_zero
- AddUnits.vaddAssocClass'_left
- AddAction.Supports.vadd
- Finset.vaddCommClass_finset'
- MeasureTheory.addFundamentalFrontier_vadd
- MeasureTheory.isAddLeftInvariant_map_vadd
- Set.vaddCommClass_set''
- Submodule.vaddCommClass
- AddOpposite.instVAddCommClass
- AddCommute.vadd_left_iff
- AddSubmonoid.instVAddCommClassSubtypeMem
- VAdd.comp.vaddCommClass'
- Function.Surjective.vaddCommClass
- VAddCommClass.op_left
- Filter.vaddCommClass_filter'
- Set.vaddCommClass
Ancestors0
No ancestors.