extendScalars — Mathlib

English

Given f: C→ₐ[A] D, extend scalars to obtain a map B→ₐ[A] D by composing with the canonical IsScalarTower map.

Русский

Имея f: C→ₐ[A] D, расширяем скаляры, получая B→ₐ[A] D через каноническое отображение IsScalarTower.

LaTeX

$$$$ extendScalars : @AlgHom B C D _ _ _ _ (f.restrictDomain B).toRingHom.toAlgebra $$$$

Lean4

/-- Extend the scalars of an `AlgHom`. -/
def extendScalars : @AlgHom B C D _ _ _ _ (f.restrictDomain B).toRingHom.toAlgebra
    where
  __ := f
  commutes' := fun _ ↦ rfl
  __ := (f.restrictDomain B).toRingHom.toAlgebra

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