isUnit — Mathlib

English

If h is a DedekindDomainInv structure on A, then every nonzero fractional ideal I is a unit.

Русский

Если структура IsDedekindDomainInv на A, то каждый не нулевой дробный идеал является единичной единицей.

LaTeX

$$$$\\text{IsDedekindDomainInv}(A) \\Rightarrow (\\forall I \\neq 0, \\ I \\text{ is a unit}).$$$$

Lean4

protected theorem isUnit {I : FractionalIdeal A⁰ K} (hI : I ≠ 0) : IsUnit I :=
  isUnit_of_mul_eq_one _ _ (h.mul_inv_eq_one hI)

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