restrictScalars_inj — Mathlib

English

Let f and g be S-linear isomorphisms between M and M₂, and suppose their restrictions to R-linear structure coincide. Then f = g. In other words, restricting scalars from S to R is an injective operation on linear equivalences.

Русский

Пусть f и g — S-линейные биективности между M и M₂; если их ограничения до структуры R-линейности совпадают, то f = g. Другими словами, ограничение скаляров по отношению к R к S инъективно отображает линейные эквививалности.

LaTeX

$$$ (\operatorname{restrict}_{R}^{S} f) = (\operatorname{restrict}_{R}^{S} g) \iff f = g $$$

Lean4

@[simp]
theorem restrictScalars_inj (f g : M ≃ₗ[S] M₂) : f.restrictScalars R = g.restrictScalars R ↔ f = g :=
  (restrictScalars_injective R).eq_iff

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