compHom — Mathlib

English

Same as above: s • x = f(s) • x, in the algebra composed with RingHom structure.

Русский

То же самое: s • x = f(s) • x, в алгебраической структуре, полученной композицией.

LaTeX

$$$s \cdot x = f(s) \cdot x$$$

Lean4

/-- Compose an `Algebra` with a `RingHom`, with action `f s • m`.

This is the algebra version of `Module.compHom`.
-/
abbrev compHom : Algebra S A where
  smul s a := f s • a
  algebraMap := (algebraMap R A).comp f
  commutes' _ _ := Algebra.commutes _ _
  smul_def' _ _ := Algebra.smul_def _ _

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