ite_one_mul — Mathlib

English

ITE distributes over multiplication with 1: ite P 1 (a b) = ite P 1 a · ite P 1 b.

Русский

Условное распределение по умножению относительно единицы: ite P 1 (a b) = ite P 1 a · ite P 1 b.

LaTeX

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

Lean4

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

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