toBoolRing_symm_eq

Mathlib.Algebra.Ring.BooleanRing

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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