genLTOne_lt_one — Mathlib

English

If H is a cyclic subgroup of a linearly ordered commutative group G, and genLTOne denotes a generator of H that lies below 1, then genLTOne is strictly less than 1: genLTOne < 1.

Русский

Пусть H — циклическая подгруппа в линейно упорядоченной коммутативной группе G, и genLTOne обозначает порождающий H элемент, лежащий ниже 1. Тогда genLTOne < 1.

LaTeX

$$$H.{\text{genLTOne}} < 1$$$

Lean4

@[to_additive negGen_neg]
theorem genLTOne_lt_one : H.genLTOne < 1 :=
  H.exists_generator_lt_one.choose_spec.1

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