ofBoolAlg_inf

Mathlib.Algebra.Ring.BooleanRing

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

English

The map ofBoolAlg sends a ⊓ b to the product: ofBoolAlg(a ⊓ b) = ofBoolAlg(a)·ofBoolAlg(b).

Русский

Отображение ofBoolAlg переводит a ⊓ b в произведение: ofBoolAlg(a ⊓ b) = ofBoolAlg(a)·ofBoolAlg(b).

LaTeX

$$$\mathrm{ofBoolAlg}(a \land b) = \mathrm{ofBoolAlg}(a) \cdot \mathrm{ofBoolAlg}(b)$$$

Lean4

@[simp]
theorem ofBoolAlg_inf (a b : AsBoolAlg α) : ofBoolAlg (a ⊓ b) = ofBoolAlg a * ofBoolAlg b :=
  rfl

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

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

Разделы

Аффилиация

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