mul_left_strictMono — Mathlib

English

If I ≠ 0 in a Dedekind domain, then the map x ↦ I · x on fractional ideals is strictly monotone.

Русский

Если I ≠ 0, то отображение x ↦ I · x на дробных идеалах строго монотонно.

LaTeX

$$$\mathrm{mul\_left\_strictMono} \bigl(\text{FractionalIdeal}(A^{\circ},K)\bigr)$$$

Lean4

theorem mul_left_strictMono [IsDedekindDomain A] {I : FractionalIdeal A⁰ K} (hI : I ≠ 0) : StrictMono (I * ·) :=
  strictMono_of_le_iff_le fun _ _ => (mul_left_le_iff hI).symm

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