mul_right_strictMono — Mathlib

English

In a Dedekind domain, multiplication by a fixed nonzero fractional ideal is strictly monotone with respect to inclusion.

Русский

Умножение на фиксированный ненулевой дробный идеал строго монотонно по включению.

LaTeX

$$$$\\text{If } I\\neq 0,\\; x \\mapsto x\\cdot I \\text{ is strictly monotone under } \\le.$$$$

Lean4

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

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