restrictScalars_injective — Mathlib

English

Restriction of scalars from S to R for StarAlgHom is injective.

Русский

Ограничение скалярного действия с S до R для StarAlgHom инъективно.

LaTeX

$$$ \\text{restrictScalars\_injective} :\\; \\text{Injective}(\\mathrm{restrictScalars}\n )$$$

Lean4

theorem restrictScalars_injective : Function.Injective (StarAlgHom.restrictScalars R : (A →⋆ₐ[S] B) → A →⋆ₐ[R] B) :=
  fun f g h => StarAlgHom.ext fun x => show f.restrictScalars R x = g.restrictScalars R x from DFunLike.congr_fun h x

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