finite_left_iff — Mathlib

English

A left transversal is finite if and only if the subgroup has finite index in G.

Русский

Левый трансплант имеет конечное множество, если и только если подгруппа имеет конечный индекс в G.

LaTeX

$$$ \text{Finite}(S) \iff [G : H] < \infty $$$

Lean4

/-- A left transversal is finite iff the subgroup has finite index. -/
@[to_additive /-- A left transversal is finite iff the subgroup has finite index. -/
    ]
theorem finite_left_iff (h : IsComplement S H) : Finite S ↔ H.FiniteIndex :=
  by
  rw [← h.leftQuotientEquiv.finite_iff]
  exact ⟨fun _ ↦ finiteIndex_of_finite_quotient, fun _ ↦ finite_quotient_of_finiteIndex⟩

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