genLTOne_mem — Mathlib

English

If g < 1 is such that Subgroup.zpowers g = H, then g is the distinguished generator of H below 1; i.e., g = H.genLTOne.

Русский

Если элемент g < 1 порождает подгруппу g-позициями: Subgroup.zpowers g = H, то такой g является единственным генератором H, лежащим ниже 1; то есть g = H.genLTOne.

LaTeX

$$$\forall g\,(g<1)\land (Subgroup.zpowers(g)=H)\Rightarrow g=H.genLTOne$$$

Lean4

theorem genLTOne_mem : H.genLTOne ∈ H :=
  by
  nth_rewrite 1 [← H.genLTOne_zpowers_eq_top]
  exact Subgroup.mem_zpowers (Subgroup.genLTOne H)

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