algHomClass — Mathlib

English

The type AlgHomClass (A →ₐ[R] B) R A B is closed under operations map_add, map_zero, map_mul, map_one, and commutes; i.e., any AlgHom class respects ring operations and scalar action.

Русский

Тип AlgHomClass (A →ₐ[R] B) обеспечивает, что операции сложения, нуля, умножения, единицы и совместимость со скалярами сохраняются; класс AlgHom сохраняет эти операции.

LaTeX

$$$\\text{AlgHomClass } (A \\toₐ[R] B) \\; R \\; A \\; B$$$

Lean4

instance algHomClass : AlgHomClass (A →ₐ[R] B) R A B
    where
  map_add f := f.map_add'
  map_zero f := f.map_zero'
  map_mul f := f.map_mul'
  map_one f := f.map_one'
  commutes f := f.commutes'

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