finite_right_iff — Mathlib

English

For a group G with a subgroup H and transversal T, T is finite iff H has finite index in G.

Русский

Для группы G с подгруппой H и трансперсантом T: T конечна тогда и только тогда, когда индекс H в G конечен.

LaTeX

$$$\\text{Finite }T \\;\\Leftrightarrow\\; H\\text{ has finite index in }G$$$

Lean4

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

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