restrictScalars₁₂_injective — Mathlib

English

If B and B′ are bilinear maps and their restricted versions coincide, then B = B′.

Русский

Если ограниченные версии двух билинейных отображений совпадают, то сами отображения совпадают.

LaTeX

$$$ B.restrictScalars₁₂ R' S' = B'.restrictScalars₁₂ R' S' \\Rightarrow B = B' $$$

Lean4

theorem restrictScalars₁₂_injective :
    Function.Injective (LinearMap.restrictScalars₁₂ R' S' : (M →ₗ[R] N →ₗ[S] Pₗ) → (M →ₗ[R'] N →ₗ[S'] Pₗ)) :=
  fun _ _ h ↦ ext₂ (congr_fun₂ h :)

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