restrictScalars_injective — Mathlib

English

Restriction of scalars is injective: if restrictScalars f = restrictScalars g then f = g.

Русский

Ограничение по скалярам вводит инъективность: если restrictScalars f = restrictScalars g, то f = g.

LaTeX

$$$\mathrm{restrictScalars}_R : (A \to_{{S}} B) \to (A \to_{{R}} B)$ is injective$$

Lean4

theorem restrictScalars_injective : Function.Injective (restrictScalars R : (A →ₐ[S] B) → A →ₐ[R] B) := fun _ _ h =>
  AlgHom.ext (AlgHom.congr_fun h :)

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