ofBoolRing_toBoolRing

Mathlib.Algebra.Ring.BooleanRing

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

English

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

Русский

Для любого a ∈ α выполняется: ofBoolRing(toBoolRing(a)) = a.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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