mul_boole

Mathlib.Algebra.Ring.Defs

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

English

Let α have a MulZeroOneClass. For any P and a, (a · ite P 1 0) = ite P a 0.

Русский

Пусть α обладает умножением с единицей. Для любого P и a верно a·ite(P,1,0) = ite(P,a,0).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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