instMulPosStrictMonoFractionalIdealNonZeroDivisors

English

Let A be a Dedekind domain and K a field with A-algebra structure and IsFractionRing A K. The left multiplication by a fixed nonzero fractional ideal is strictly monotone with respect to inclusion on fractional ideals.

Русский

Пусть A — детерминантный домен, K — поле, дано отображение A → K и структура алгебры. Левое умножение фиксированным ненулевым дробным идеалом является строго монотонным по включению дробных идеалов.

LaTeX

$$$\mathrm{MulPosStrictMono}\bigl(\mathrm{FractionalIdeal}(A^{\circ},K)\bigr)$$$

Lean4

instance : MulPosStrictMono (FractionalIdeal A⁰ K) :=
  MulPosMono.toMulPosStrictMono

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