asBoolAlg_comp

Mathlib.Algebra.Ring.BooleanRing

URI: https://scilib.ai/kg/mathlib#RingHom.asBoolAlg_comp

Lean4

@[simp]
theorem asBoolAlg_comp (g : β →+* γ) (f : α →+* β) : (g.comp f).asBoolAlg = g.asBoolAlg.comp f.asBoolAlg :=
  rfl

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

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

Разделы

Аффилиация

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