Theorems · Inductive type · group theory
MulAction.QuotientAction
{G : Type u} → (X : Type v) → [inst : Group G] → [inst_1 : Monoid X] → [MulAction X G] → Subgroup G → PropA typeclass for when a MulAction X G descends to the quotient G ⧸ H.
- Defined in
- Mathlib.GroupTheory.GroupAction.Quotient
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by10
Results whose statement or proof uses this declaration.
- Subgroup.smul_apply_eq_smul_apply_inv_smulstatement and proof · cited by 4
- MulAction.Quotient.mk_smul_outstatement and proof · cited by 2
- MulAction.Quotient.smul_mkstatement and proof · cited by 2
- MulAction.Quotient.coe_smul_outstatement and proof · cited by 1
- MulAction.Quotient.smul_coestatement and proof · cited by 1
- Subgroup.smul_leftQuotientEquivstatement and proof · cited by 1
- MulAction.QuotientAction.inv_mul_memstatement and proof · cited by 1
- Subgroup.smul_toLeftFunstatement and proof · cited by 1
- MulAction.QuotientAction.casesOnstatement and proof · cited by 0
- MulAction.QuotientAction.recOnstatement and proof · cited by 0