algHom_evalAlgHom

Mathlib.Algebra.Algebra.Pi

URI: https://scilib.ai/kg/mathlib#Pi.algHom_evalAlgHom

English

The canonical Pi-algebra homomorphism composed with evaluation equals the identity on the product.

Русский

Существует равенство: композиция Pi-algHom с evalAlgHom равна тождественному отображению на произведение.

LaTeX

$$$ algHom R A (evalAlgHom R A) = AlgHom.id R (\\prod_i A_i) $$$

Lean4

@[simp]
theorem algHom_evalAlgHom : algHom R A (evalAlgHom R A) = AlgHom.id R (Π i, A i) :=
  rfl

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

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

Разделы

Аффилиация

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