ofBoolRing_mul

Mathlib.Algebra.Ring.BooleanRing

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

English

For any a,b ∈ AsBoolRing α,

Русский

Для любых a,b ∈ AsBoolRing α выполняется: ofBoolRing(a b) = ofBoolRing(a) ∧ ofBoolRing(b).

LaTeX

$$$\operatorname{ofBoolRing}(a b) = \operatorname{ofBoolRing}(a) \land \operatorname{ofBoolRing}(b).$$$

Lean4

@[simp]
theorem ofBoolRing_mul (a b : AsBoolRing α) : ofBoolRing (a * b) = ofBoolRing a ⊓ ofBoolRing b :=
  rfl

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

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

Разделы

Аффилиация

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