boole_mul

Mathlib.Algebra.Ring.Defs

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

English

The left distribution by a boolean condition: (if P then 1 else 0) · a = if P then a else 0.

Русский

Левое распределение по условию: (если P, то 1, иначе 0) · a = если P, то a, иначе 0.

LaTeX

$$$ \text{ite}(P,1,0) \cdot a = \text{ite}(P,a,0) $$$

Lean4

theorem boole_mul {α} [MulZeroOneClass α] (P : Prop) [Decidable P] (a : α) :
    (if P then 1 else 0) * a = if P then a else 0 := by simp

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

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

Разделы

Аффилиация

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