unitGroup_strictMono

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.unitGroup_strictMono

English

The map A ↦ A.unitGroup is strictly monotone: if A < B then A.unitGroup < B.unitGroup.

Русский

Отображение A ↦ A.unitGroup строго монотонно: если A < B, то A.unitGroup < B.unitGroup.

LaTeX

$$A < B \Rightarrow A_{\mathrm{unitGroup}} < B_{\mathrm{unitGroup}}$$

Lean4

theorem unitGroup_strictMono : StrictMono (unitGroup : ValuationSubring K → Subgroup _) :=
  unitGroupOrderEmbedding.strictMono

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru