noZeroSMulDivisors — Mathlib

English

If R has no zero divisors, then the free R-module M has NoZeroSmulDivisors as an R-module.

Русский

Если кольцо R не содержит делителей нуля, то свободный модуль над R имеет свойство NoZeroSmulDivisors как модуль над R.

LaTeX

$$$$ [NoZeroDivisors\ R] \Rightarrow [NoZeroSMulDivisors\ R\ M] $$$$

Lean4

instance (priority := 100) noZeroSMulDivisors [NoZeroDivisors R] : NoZeroSMulDivisors R M :=
  let ⟨⟨_, b⟩⟩ := exists_basis (R := R) (M := M)
  b.noZeroSMulDivisors

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