eq_iff_unitGroup

Mathlib.RingTheory.Valuation.ValuationSubring

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

English

Two valuation subrings A and B are equal if and only if their unit groups are equal.

Русский

Два valuation-подкольца A и B равны тогда и только тогда, когда их группы единиц равны.

LaTeX

$$$A = B \iff A_{\mathrm{unitGroup}} = B_{\mathrm{unitGroup}}$$$

Lean4

theorem eq_iff_unitGroup {A B : ValuationSubring K} : A = B ↔ A.unitGroup = B.unitGroup :=
  unitGroup_injective.eq_iff.symm

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

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

Разделы

Аффилиация

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