instBooleanRingCarrierToBddLatToBddDistLatOfAsBoolAlg

Mathlib.Algebra.Category.BoolRing

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

Lean4

instance {R : Type u} [BooleanRing R] : BooleanRing (BoolAlg.of (AsBoolAlg ↑R)).toBddDistLat.toBddLat.toLat :=
  inferInstanceAs <| BooleanRing R

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

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

Разделы

Аффилиация

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