ofBoolRing_add — Mathlib

English

Addition in AsBoolRing corresponds to symmetric difference on the underlying set; i.e., ofBoolRing(a + b) = ofBoolRing(a) △ ofBoolRing(b).

Русский

Сложение в AsBoolRing соответствует симметрической разности на базовом множестве: ofBoolRing(a + b) = ofBoolRing(a) △ ofBoolRing(b).

LaTeX

$$$\operatorname{ofBoolRing}(a + b) = \operatorname{ofBoolRing}(a) \triangle \operatorname{ofBoolRing}(b)$$$

Lean4

@[simp]
theorem ofBoolRing_add (a b : AsBoolRing α) : ofBoolRing (a + b) = ofBoolRing a ∆ ofBoolRing b :=
  rfl

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