integralRep — Mathlib

English

There is a notion of an integral representative of a fractional ideal, obtained by taking its numerator.

Русский

Существует интегральный представитель дробного идеала, получаемый через его числитель.

LaTeX

$$$\mathrm{ClassGroup.integralRep}(I) = \mathrm{num}(I)$$$

Lean4

/-- Maps a nonzero fractional ideal to an integral representative in the class group. -/
noncomputable def integralRep (I : FractionalIdeal R⁰ (FractionRing R)) : Ideal R :=
  I.num

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