den — Mathlib

English

The denominator of a fractional ideal is a fixed nonzero element of S whose class provides a cancellation relationship.

Русский

Поскольку деноминатор дробного идеала — некоторое ненулевое элемент S, задающее отношение редукции.

LaTeX

$$$I.den \\in S$$$

Lean4

/-- An element of `S` such that `I.den • I = I.num`, see `FractionalIdeal.num` and
`FractionalIdeal.den_mul_self_eq_num`. -/
noncomputable def den (I : FractionalIdeal S P) : S :=
  ⟨I.2.choose, I.2.choose_spec.1⟩

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