principalUnitGroup_injective — Mathlib

English

The map sending a valuation subring to its principal unit group is injective; i.e., if two valuation subrings have the same principal unit group, they are equal.

Русский

Отображение, отправляющее ценностное подполько к его главной группe единиц, является инъективным; если две ценностные подкольца имеют одинаковую главную группу единиц, они совпадают.

LaTeX

$$$\forall A,B:\mathrm{ValuationSubring}(K),\ A.principalUnitGroup = B.principalUnitGroup \Rightarrow A = B$$$

Lean4

theorem principalUnitGroup_injective : Function.Injective (principalUnitGroup : ValuationSubring K → Subgroup _) :=
  fun A B h => by simpa [le_antisymm_iff, principalUnitGroup_le_principalUnitGroup] using h.symm

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