coe_restrictScalars — Mathlib

English

The underlying ring homomorphism of restrictScalars equals the original algebra homomorphism when viewed as a ring hom.

Русский

Базовое кольцевое отображение restrictScalars совпадает с исходным алгебра-гомоморфизмом, если рассматривать как кольцевой гомоморфизм.

LaTeX

$$$ (restrictScalars\ R\ f: A \to B) = f$$$

Lean4

@[simp]
theorem coe_restrictScalars (f : A →ₐ[S] B) : (f.restrictScalars R : A →+* B) = f :=
  rfl

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