fintypeQuotientOfFiniteIndex — Mathlib

English

If H has finite index, then Fintype (HasQuotient.Quotient G H).

Русский

Если у H конечный индекс, то имеется Fintype квотиенты G/H.

LaTeX

$$[FiniteIndex H] ⇒ Fintype(HasQuotient.Quotient G H)$$

Lean4

/-- A finite index subgroup has finite quotient. -/
@[to_additive /-- A finite index subgroup has finite quotient -/
    ]
noncomputable def fintypeQuotientOfFiniteIndex [FiniteIndex H] : Fintype (G ⧸ H) :=
  fintypeOfIndexNeZero FiniteIndex.index_ne_zero

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