Theorems · Inductive type · group theory

AddAction.QuotientAction

{G : Type u} → (X : Type v) → [inst : AddGroup G] → [inst_1 : AddMonoid X] → [AddAction X G] → AddSubgroup G → Prop

A typeclass for when an AddAction 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

Assumes

AddGroupAddMonoidAddAction