linearMapClass — Mathlib

English

Any type F equipped with an AlgHomClass structure automatically forms a LinearMapClass with respect to R-algebras A and B; the map respects scalar multiplication.

Русский

Любой тип F, имеющий структуру AlgHomClass, автоматически образует LinearMapClass по отношению к R-алгебрам A и B; отображение сохраняет скаляры.

LaTeX

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

Lean4

instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass F R A B :=
  { ‹AlgHomClass F R A B› with
    map_smulₛₗ := fun f r x => by simp only [Algebra.smul_def, map_mul, commutes, RingHom.id_apply] }

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