toAlgHomClass — Mathlib

English

If F carries an AlgEquivClass for R-algebras A and B, then F forms a class of R-algebra homomorphisms from A to B.

Русский

Если F обладает структурой AlgEquivClass для R-алгебр A и B, то F образует класс R-алгебровых гомоморфизмов A → B.

LaTeX

$$$\\text{AlgHomClass } F\\; R\\; A\\; B$$$

Lean4

instance (priority := 100) toAlgHomClass (F R A B : Type*) [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
    [Algebra R B] [EquivLike F A B] [h : AlgEquivClass F R A B] : AlgHomClass F R A B :=
  { h with }

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