nonunits_injective — Mathlib

English

The map nonunits: ValuationSubring K → Subsemigroup K is injective; i.e., A.nonunits = B.nonunits implies A = B.

Русский

Отображение nonunits: ValuationSubring K → Subsemigroup K инъективно; то есть A.nonunits = B.nonunits → A = B.

LaTeX

$$A_{nonunits} = B_{nonunits} \Rightarrow A = B$$

Lean4

theorem nonunits_injective : Function.Injective (nonunits : ValuationSubring K → Subsemigroup _) := fun A B h => by
  simpa only [le_antisymm_iff, nonunits_le_nonunits] using h.symm

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