span_singleton_mul_right_mono — Mathlib

English

In a domain, for x ≠ 0, I ≤ J iff span{x} · I ≤ span{x} · J.

Русский

В области domain, при x ≠ 0, I ≤ J эквивалентно span{x} · I ≤ span{x} · J.

LaTeX

$$$ [IsDomain\\, R] {x : R} (hx : x \\neq 0) : I ≤ J \\iff span{ x } · I ≤ span{ x } · J $$$

Lean4

theorem span_singleton_mul_right_mono [IsDomain R] {x : R} (hx : x ≠ 0) : span { x } * I ≤ span { x } * J ↔ I ≤ J := by
  simp_rw [span_singleton_mul_le_span_singleton_mul, mul_right_inj' hx, exists_eq_right', SetLike.le_def]

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