mul_left_mono — Mathlib

English

Right multiplication by a fixed fractional ideal I is monotone: if J ≤ J', then J · I ≤ J' · I.

Русский

Правое умножение на фиксированный дробный идеал I монотонно: если J ≤ J', то J · I ≤ J' · I.

LaTeX

$$Monotone fun J => J * I$$

Lean4

theorem mul_left_mono (I : FractionalIdeal S P) : Monotone (I * ·) :=
  by
  intro J J' h
  simp only [mul_def]
  exact mul_le.mpr fun x hx y hy => mul_mem_mul hx (h hy)

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