num — Mathlib

English

The numerator of a FractionalIdeal is an associated ideal of R embedded in P.

Русский

Числитель дробного идеала является ассоциированным идеалом R, внедрённым в P.

LaTeX

$$$I.num := (I.den \\cdot I)\\text{ подмодуль } R$$$

Lean4

/-- An ideal of `R` such that `I.den • I = I.num`, see `FractionalIdeal.den` and
`FractionalIdeal.den_mul_self_eq_num`. -/
noncomputable def num (I : FractionalIdeal S P) : Ideal R :=
  (I.den • (I : Submodule R P)).comap (Algebra.linearMap R P)

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