toBoolRing_ofBoolRing — Mathlib

English

For any a ∈ AsBoolRing α, applying toBoolRing after ofBoolRing returns a: toBoolRing(ofBoolRing(a)) = a.

Русский

Для любого a ∈ AsBoolRing α применение toBoolRing после ofBoolRing возвращает a: toBoolRing(ofBoolRing(a)) = a.

LaTeX

$$$\forall a \in AsBoolRing(\alpha),\; \operatorname{toBoolRing}(\operatorname{ofBoolRing}(a)) = a.$$$

Lean4

@[simp]
theorem toBoolRing_ofBoolRing (a : AsBoolRing α) : toBoolRing (ofBoolRing a) = a :=
  rfl

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