English
Let R be a ring and M an R-module with NoZeroSmulDivisors. For x, y in M, the equality of the spans R·x = R·y holds if and only if there exists a unit z ∈ R× such that z·x = y.
Русский
Пусть R — кольцо, M — модуль над R и выполняются условия NoZeroSmulDivisors(R, M). Пусть x, y ∈ M. Подмодули, порожденные единичными элементами x и y, равны тогда и только тогда, когда существует еденица-знаменитость z ∈ R× такая, что z·x = y.
LaTeX
$$$$ \\operatorname{span}_R(\\{x\\}) = \\operatorname{span}_R(\\{y\\}) \\quad \\Longleftrightarrow\\quad \\exists z \\in R^{\\times},\\ z\\cdot x = y.$$$$
Lean4
theorem span_singleton_eq_span_singleton {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
{x y : M} : ((R ∙ x) = R ∙ y) ↔ ∃ z : Rˣ, z • x = y :=
by
constructor
· simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]
rintro ⟨⟨a, rfl⟩, b, hb⟩
rcases eq_or_ne y 0 with rfl | hy; · simp
refine ⟨⟨b, a, ?_, ?_⟩, hb⟩
· apply smul_left_injective R hy
simpa only [mul_smul, one_smul]
· rw [← hb] at hy
apply smul_left_injective R (smul_ne_zero_iff.1 hy).2
simp only [mul_smul, one_smul, hb]
· rintro ⟨u, rfl⟩
exact (span_singleton_group_smul_eq _ _ _).symm
