instNoZeroSMulDivisors — Mathlib

English

If R has a zero and ENNReal scalars act on measures with no-zero smul divisors, then Measure α also has NoZeroSmulDivisors: if c ≠ 0 and c • μ = 0, then μ = 0.

Русский

Если есть нуль в R и не нулевые делители умножения на ENNReal действуют на меры, то мерам S также свойственно свойство NoZeroSmulDivisors: если c ≠ 0 и c • μ = 0, то μ = 0.

LaTeX

$$$\forall c:\, R,\, c \neq 0 \Rightarrow (c \cdot \mu = 0) \Rightarrow \mu = 0.$$$

Lean4

instance instNoZeroSMulDivisors [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] [NoZeroSMulDivisors R ℝ≥0∞] :
    NoZeroSMulDivisors R (Measure α) where
  eq_zero_or_eq_zero_of_smul_eq_zero h := by simpa [Ne, ext_iff', forall_or_left] using h

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