isCongruenceSubgroup_trans — Mathlib

English

If H ≤ K and H is a congruence subgroup, then K is a congruence subgroup.

Русский

Если H подмножество K и H является конгруэнционной подгруппой, то K также конгруэнционная подгруппа.

LaTeX

$$$$ H \leq K \quad \text{and} \quad \text{IsCongruenceSubgroup}(H) \quad \Longrightarrow \quad \text{IsCongruenceSubgroup}(K). $$$$

Lean4

theorem isCongruenceSubgroup_trans (H K : Subgroup SL(2, ℤ)) (h : H ≤ K) (h2 : IsCongruenceSubgroup H) :
    IsCongruenceSubgroup K := by
  obtain ⟨N, hN⟩ := h2
  exact ⟨N, hN.1, hN.2.trans h⟩

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