genLTOne_zpowers_eq_top — Mathlib

English

The cyclic subgroup H is exactly the subgroup generated by genLTOne, i.e. H = Subgroup.zpowers(genLTOne).

Русский

Циклическая подгруппа H равна подгруппе, порождаемой genLTOne: H = Subgroup.zpowers(genLTOne).

LaTeX

$$$\operatorname{zpowers}(\,genLTOne\, ) = H$$$

Lean4

@[to_additive (attr := simp) negGen_zmultiples_eq_top]
theorem genLTOne_zpowers_eq_top : Subgroup.zpowers H.genLTOne = H :=
  H.exists_generator_lt_one.choose_spec.2

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