mul_left_le_iff — Mathlib

English

In a Dedekind domain, for J ≠ 0, I·J ≤ I'·J iff I ≤ I' (left-cancel by J).

Русский

В Дедекинд домене, для J ≠ 0, I·J ≤ I'·J эквивалентно I ≤ I' (левый отмена по J).

LaTeX

$$$$\\forall J\\neq 0:\\; (I \\cdot J \\le I' \\cdot J) \\iff (I \\le I').$$$$

Lean4

theorem mul_left_le_iff [IsDedekindDomain A] {J : FractionalIdeal A⁰ K} (hJ : J ≠ 0) {I I'} : J * I ≤ J * I' ↔ I ≤ I' :=
  by convert mul_right_le_iff hJ using 1; simp only [mul_comm]

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