instAlgHomClass — Mathlib

English

There is a canonical AlgHomClass structure on ContinuousAlgHom R A B, so that any ContinuousAlgHom behaves like an AlgHom in terms of multiplication, addition, and identity, with commutativity preserved.

Русский

Существует каноническая структура AlgHomClass на ContinuousAlgHom R A B, чтобы любые ContinuousAlgHom вели себя как AlgHom относительно умножения, сложения и единицы, сохраняя коммутативность.

LaTeX

$$$\\text{AlgHomClass} (ContinuousAlgHom\\ R\\ A\\ B)\\ R\\ A\\ B$$$

Lean4

instance : AlgHomClass (A →A[R] B) R A B
    where
  map_mul f x y := map_mul f.toAlgHom x y
  map_one f := map_one f.toAlgHom
  map_add f := map_add f.toAlgHom
  map_zero f := map_zero f.toAlgHom
  commutes f r := f.toAlgHom.commutes r

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