restrictScalars_injective — Mathlib

English

The underlying function after restricting scalars equals the original function viewed as a map A → B.

Русский

После ограничения скаляров функция равна исходной функции как отображение A → B.

LaTeX

$$$\\big( f\\restrict_R\\big) : A\\to B = f$$$

Lean4

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

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