instHasQuotientSubgroup — Mathlib

English

For any subgroup s of α, the quotient α / s exists as a quotient type (has well-defined left cosets).

Русский

Для любой подгруппы s группы α существует фактор-группа α / s (множество левых косет).

LaTeX

$$HasQuotient α (Subgroup α)$$

Lean4

/-- `α ⧸ s` is the quotient type representing the left cosets of `s`. If `s` is a normal subgroup,
`α ⧸ s` is a group -/
@[to_additive /-- `α ⧸ s` is the quotient type representing the left cosets of `s`. If `s` is a
    normal subgroup, `α ⧸ s` is a group -/
    ]
instance instHasQuotientSubgroup : HasQuotient α (Subgroup α) :=
  ⟨fun s => Quotient (leftRel s)⟩

Похожие утверждения