Structures · Algebra
MulAction.QuotientAction
A typeclass for when a MulAction 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
- Subgroup.smul_apply_eq_smul_apply_inv_smul
- MulAction.Quotient.smul_mk
- MulAction.Quotient.mk_smul_out
- MulAction.Quotient.coe_smul_out
- MulAction.QuotientAction.inv_mul_mem
- MulAction.Quotient.smul_coe
- Subgroup.smul_leftQuotientEquiv
- Subgroup.smul_toLeftFun
- MulAction.quotient
- Subgroup.instMulActionLeftTransversal
Ancestors0
No ancestors.