boole_smul

Mathlib.Algebra.GroupWithZero.Action.Defs

URI: https://scilib.ai/kg/mathlib#boole_smul

English

For any a ∈ A, (if p then 1 else 0) • a equals if p then a else 0.

Русский

Для любого a ∈ A, (если p то 1 иначе 0) • a равняется если p тогда a иначе 0.

LaTeX

$$$\\text{boole\_smul} \\ (a:\\, A) : (\\mathrm{ite}\\ p\\ 1\\ 0) \\cdot a = \\mathrm{ite}\\ p\\ a\\ 0$$$

Lean4

theorem boole_smul (a : A) : (if p then 1 else 0 : M₀) • a = if p then a else 0 := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru