Structures · Algebra
IsCentralVAdd
A typeclass indicating that the right (aka AddOpposite) and left actions by M on α are
equal, that is that M acts centrally on α. This can be thought of as a version of commutativity
for +ᵥ.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Shape
- 2 explicit arguments · adds op_vadd_eq_vadd
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by28
- IsCentralVAdd.op_vadd_eq_vadd
- IsCentralVAdd.unop_vadd_eq_vadd
- UniformSpace.Completion.instIsCentralVAdd
- Set.isCentralVAdd
- Finset.isCentralVAdd
- AddOpposite.unop_vadd_eq_unop_vadd_unop
- Sum.instIsCentralVAdd
- AddOreLocalization.instIsCentralVAdd
- AddOpposite.instMeasurableConstVAdd
- SeparationQuotient.instIsCentralVAdd
- Prod.isCentralVAdd
- VAddCommClass.op_left
- IsIsometricVAdd.opposite_of_comm
- VAddAssocClass.op_right
- Filter.isCentralVAdd
- VAddAssocClass.op_left
- AddOpposite.op_vadd_eq_op_vadd_op
- VAddCommClass.op_right
- Option.instIsCentralVAdd
- ContinuousConstVAdd.op
- Equiv.isCentralVAdd
- AddOpposite.instIsCentralVAdd
- UniformContinuousConstVAdd.op
- MeasurableVAdd.op
- ContinuousVAdd.op
- Sigma.instIsCentralVAdd
- Pi.isCentralVAdd
- SubAddAction.isCentralVAdd
Ancestors0
No ancestors.