genLTOne_eq_of_top — Mathlib

English

For a cyclic group G, the generator below 1 of G equals the generator below 1 of the top subgroup, i.e. genLTOne G = genLTOne ⊤.

Русский

Для циклической группы G порождающий элемент ниже 1 равен порождающему элементу для верхней подгруппы: genLTOne G = genLTOne ⊤.

LaTeX

$$$\text{genLTOne}(G) = \text{genLTOne}(\top)$$$

Lean4

@[to_additive (attr := simp) negGen_eq_of_top]
theorem genLTOne_eq_of_top : genLTOne G = (⊤ : Subgroup G).genLTOne :=
  rfl

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