Structures · Algebra
VAddAssocClass
An instance of VAddAssocClass M N α states that the additive action of M on α is
determined by the additive actions of M on N and N on α.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Shape
- 3 explicit arguments · adds vadd_assoc
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances8
- AddUnits
- Subtype
- OrderDual
- Lex
- AddOpposite
- Set
- Finset
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by116
- vadd_assoc
- vadd_zero_vadd
- vadd_add_assoc
- VAddAssocClass.vadd_assoc
- AddSemiconjBy.vadd_right
- AddOreLocalization.vadd_oreSub
- vadd_vadd_vadd_comm
- CovByVAdd.trans
- faithfulVAdd_iff_injective_vadd_zero
- AddSemiconjBy.vadd_left
- vadd_add_vadd_comm
- AddSemiconjBy.vadd_right_iff
- AddAction.le_stabilizer_vadd_left
- AddMonoidHom.vaddZeroHom
- AddOreLocalization.vadd_zero_oreSub_zero_vadd
- vadd_add_vadd
- vadd_zero_add
- SubAddAction.vadd_of_tower_mem
- AddOreLocalization.vadd_zero_vadd
- List.vadd_sum
- AddUnits.val_vadd
- AddSemiconjBy.vadd_left_iff
- AddAction.stabilizer_vadd_eq_left
- Finset.vaddAssocClass
- AddCommute.vadd_left
- UniformSpace.Completion.instVAddAssocClass
- Equiv.vaddAssocClass
- AddCon.instVAdd
- Set.vaddAssocClass
- AddAction.isBlock_addSubgroup
- SubAddAction.val_vadd_of_tower
- FaithfulVAdd.tower_bot
- AddAction.IsPretransitive.of_vaddAssocClass
- AddSubgroup.instVAddAssocClassSubtypeMem
- VAdd.comp.vaddAssocClass
- AddOpposite.instVAddAssocClass
- VAddAssocClass.to₁₃₄
- AddOreLocalization.instAddActionOfVAddAssocClass
- AddUnits.vadd_neg
- SetLike.vadd'
- AddUnits.instVAddAssocClass
- AddOreLocalization.vadd_oreSub_zero
- AddUnits.vaddCommClass'
- SeparationQuotient.instVAddAssocClass
- Pi.vaddAssocClass
- AddOreLocalization.instIsCentralVAdd
- AddAction.isBlock_addSubgroup'
- AddUnits.vaddAssocClass'_left
- AddOreLocalization.instVAddOfVAddAssocClass
- AddConstMap.instAddActionOfVAddAssocClass
Ancestors0
No ancestors.