instFiniteIndex_subgroupOf — Mathlib

English

If H ≤ G has finite index, then H.subgroupOf K has finite index in H (i.e., [H : H ∩ K] < ∞).

Русский

Если H ≤ G имеет конечный индекс, то H.subgroupOf K имеет конечный индекс в H (то есть [H : H ∩ K] < ∞).

LaTeX

$$(H ∩ K).FiniteIndex$$

Lean4

@[to_additive]
instance instFiniteIndex_subgroupOf (H K : Subgroup G) [H.FiniteIndex] : (H.subgroupOf K).FiniteIndex :=
  ⟨fun h => H.index_ne_zero_of_finite <| H.index_eq_zero_of_relIndex_eq_zero h⟩

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