ite_mul_one

Mathlib.Algebra.Group.Basic

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

English

For MulOneClass M, ite P (a b) 1 = (ite P a 1) (ite P b 1).

Русский

Для множества с единицей µ верно: условное умножение ite(P, a b) 1 равно (ite(P, a, 1)) (ite(P, b, 1)).

LaTeX

$$$\mathrm{ite}(P, a\,b, 1) = \mathrm{ite}(P, a, 1) \cdot \mathrm{ite}(P, b, 1)$$$

Lean4

@[to_additive]
theorem ite_mul_one {P : Prop} [Decidable P] {a b : M} : ite P (a * b) 1 = ite P a 1 * ite P b 1 := by
  by_cases h : P <;> simp [h]

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

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

Разделы

Аффилиация

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