noZeroSMulDivisors — Mathlib

English

If R, M, N are types with zero and SMulWithZero and if NoZeroSMulDivisors holds for M and for N, then it holds for M × N.

Русский

Пусть есть нули и скалярное умножение на M и N; если для M и для N выполняются NoZeroSMulDivisors, то это верно и для произведения M × N.

LaTeX

$$$$NoZeroSMulDivisors\,R\,(M) \land NoZeroSMulDivisors\,R\,(N) \Rightarrow NoZeroSMulDivisors\,R\,(M \times N).$$$$

Lean4

instance noZeroSMulDivisors [Zero R] [Zero M] [Zero N] [SMulWithZero R M] [SMulWithZero R N] [NoZeroSMulDivisors R M]
    [NoZeroSMulDivisors R N] : NoZeroSMulDivisors R (M × N) where
  eq_zero_or_eq_zero_of_smul_eq_zero {c xy} h := by simpa [Prod.ext_iff, or_and_left] using h

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