toBoolRing_symmDiff

Mathlib.Algebra.Ring.BooleanRing

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

English

For any a,b ∈ α, toBoolRing(a ∆ b) = toBoolRing(a) + toBoolRing(b).

Русский

Для любых a,b ∈ α: toBoolRing(a ∆ b) = toBoolRing(a) + toBoolRing(b).

LaTeX

$$$\operatorname{toBoolRing}(a \Delta b) = \operatorname{toBoolRing}(a) + \operatorname{toBoolRing}(b).$$$

Lean4

@[simp]
theorem toBoolRing_symmDiff (a b : α) : toBoolRing (a ∆ b) = toBoolRing a + toBoolRing b :=
  rfl

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

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

Разделы

Аффилиация

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