ofBoolRing_symm_eq

Mathlib.Algebra.Ring.BooleanRing

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

English

The inverse of ofBoolRing equals toBoolRing, i.e., (ofBoolRing)^{-1} = toBoolRing.

Русский

Обратное отображение к ofBoolRing равно toBoolRing, то есть (ofBoolRing)^{-1} = toBoolRing.

LaTeX

$$$\left(\operatorname{ofBoolRing}\right)^{-1} = \operatorname{toBoolRing}.$$$

Lean4

@[simp]
theorem ofBoolRing_symm_eq : (@ofBoolRing α).symm = toBoolRing :=
  rfl

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

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

Разделы

Аффилиация

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