smul_ite_zero — Mathlib

English

For any proposition p, and elements a ∈ M, b ∈ A, a • (if p then b else 0) equals (if p then a • b else 0).

Русский

Для любого утверждения p и элементов a ∈ M, b ∈ A, выполняется a • (если p тогда b иначе 0) = (если p тогда a • b иначе 0).

LaTeX

$$$\\forall p\\, (\\text{Decidable } p)\\; (a:\\, M)\\; (b:\\, A),\\quad a \\cdot (\\mathrm{ite}\\ p\\ b\\ 0) = \\mathrm{ite}\\ p\\ (a \\cdot b)\\ 0$$$

Lean4

theorem smul_ite_zero (p : Prop) [Decidable p] (a : M) (b : A) : (a • if p then b else 0) = if p then a • b else 0 := by
  split_ifs <;> simp

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