Structures · Algebra
AddDistribAddAction
Typeclass for additive actions on additive structures.
The key axiom here is vadd_add : g +ᵥ (x + y) = (g +ᵥ x) + (g +ᵥ y).
If G is an additive group with additive automorphism group Γ, then there is a natural instance
of AddDistribAddAction Γ G.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Shape
- 2 explicit arguments · adds vadd_zero, vadd_add
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- AddAut
How is a type an instance?
Loading the hierarchy index…