English
If R has no zero divisors, then for any basis b, no zero-scalar can annihilate a nonzero vector in M.
Русский
Если у кольца R нет нулевых делителей, то для любого базиса b и любого ненулевого вектора x в M, не существует ненулевого c ∈ R с c·x = 0.
LaTeX
$$$\\forall\\{c:\\,R\\}\\{x:\\,M\\}, c\\cdot x = 0 \\Rightarrow c = 0 \\lor x = 0$$$
Lean4
protected theorem noZeroSMulDivisors [NoZeroDivisors R] (b : Basis ι R M) : NoZeroSMulDivisors R M :=
⟨fun {c x} hcx => by
exact
or_iff_not_imp_right.mpr fun hx =>
by
rw [← b.linearCombination_repr x, ← LinearMap.map_smul, ← map_zero (linearCombination R b)] at hcx
have := b.linearIndependent hcx
rw [smul_eq_zero] at this
exact this.resolve_right fun hr => hx (b.repr.map_eq_zero_iff.mp hr)⟩
