_example

Mathlib.Algebra.Algebra.Pi

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

English

One can view constant functions as an algebra homomorphism from the scalar algebra B to the function space A → B.

Русский

Константные функции рассматриваются как алгебра-хомоморфизм из скалярной алгебры B в пространство функций A → B.

LaTeX

$$$ constAlgHom : B \\to_{Alg,R} (A \\to B) $$$

Lean4

example : Pi.instAlgebraForall S S = Algebra.id _ :=
  rfl

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

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

Разделы

Аффилиация

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