ite_zero_smul — Mathlib

English

If p is a decidable proposition, then (ite p a 0) acts on b as ite p (a • b) 0.

Русский

Пусть p разрешимо; тогда (ite p a 0) действует на b так, как если p тру, то a • b, иначе 0.

LaTeX

$$$\\text{ite\_zero\_smul} \\ (a:\\, M_0)\\ (b:\\, A) : (\\mathrm{ite}\\ p\\ a\\ 0) \\cdot b = \\mathrm{ite}\\ p\\ (a \\cdot b)\\ 0$$$

Lean4

theorem ite_zero_smul (a : M₀) (b : A) : (if p then a else 0 : M₀) • b = if p then a • b else 0 := by
  rw [ite_smul, zero_smul]

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