ofBoolRing — Mathlib

English

There is an identity equivalence between AsBoolRing α and α, i.e., AsBoolRing α is canonically identified with α.

Русский

Существует тождественная эквивалентность между AsBoolRing α и α, то есть AsBoolRing α канонически идентичен α.

LaTeX

$$$\operatorname{ofBoolRing} : AsBoolRing(α) \simeq α,$ and $\operatorname{toBoolRing}$ is its inverse with $\operatorname{toBoolRing} \circ \operatorname{ofBoolRing} = \mathrm{id}$ and $\operatorname{ofBoolRing} \circ \operatorname{toBoolRing} = \mathrm{id}$.$$

Lean4

/-- The "identity" equivalence between `α` and `AsBoolRing α`. -/
def ofBoolRing : AsBoolRing α ≃ α :=
  Equiv.refl _

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