Structures · Algebra
AddAction.QuotientAction
A typeclass for when an AddAction X G descends to the quotient G ⧸ H.
- Defined in
- Mathlib.GroupTheory.GroupAction.Quotient
- Shape
- 2 explicit arguments · adds inv_mul_mem
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 by10
- AddAction.Quotient.vadd_coe
- AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd
- AddSubgroup.vadd_toLeftFun
- AddAction.QuotientAction.inv_mul_mem
- AddAction.Quotient.mk_vadd_out
- AddAction.Quotient.coe_vadd_out
- AddSubgroup.vadd_leftQuotientEquiv
- AddAction.Quotient.vadd_mk
- AddAction.quotient
- AddSubgroup.instAddActionLeftTransversal
Ancestors0
No ancestors.