valueGroup_genLTOne_eq_generator — Mathlib

English

The substructure of the value group generated by elements below 1 coincides with the distinguished generator of the valuation.

Русский

Подгруппа значений группы значений, порождаемая элементами меньше единицы, совпадает с порождающим элементом.v

LaTeX

$$$(\mathrm{valueGroup}(v)).\mathrm{genLTOne} = \mathrm{generator}(v)$$$

Lean4

theorem valueGroup_genLTOne_eq_generator : (valueGroup v).genLTOne = generator v :=
  ((valueGroup v).genLTOne_unique (generator_lt_one v) (generator_zpowers_eq_valueGroup v)).symm

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