span_singleton_mul_right_inj — Mathlib

English

If x ≠ 0 in a domain, then Span{x} · I = Span{x} · J implies I = J.

Русский

Если x ≠ 0 в области, то Span{x} · I = Span{x} · J влечёт I = J.

LaTeX

$$$ [IsDomain\\, R] \\{x : R\\} (hx : x \\neq 0) : I \\cdot span{ x } = J \\cdot span{ x } \\Rightarrow I = J $$$

Lean4

theorem span_singleton_mul_right_inj [IsDomain R] {x : R} (hx : x ≠ 0) : span { x } * I = span { x } * J ↔ I = J := by
  simp only [le_antisymm_iff, span_singleton_mul_right_mono hx]

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