restrictScalars₁₂_inj — Mathlib

English

A formalized injectivity statement: restricting two bilinear maps with id rings yields an equivalence implying equality.

Русский

Формулируемое утверждение о инъективности: ограничение билинейных отображений сохраняет различия.

LaTeX

$$$ (B \\text{ restricted}) = (B' \\text{ restricted}) \\Rightarrow B = B' $$$

Lean4

@[simp]
theorem restrictScalars₁₂_inj {B B' : M →ₗ[R] N →ₗ[S] Pₗ} :
    B.restrictScalars₁₂ R' S' = B'.restrictScalars₁₂ R' S' ↔ B = B' :=
  (restrictScalars₁₂_injective R' S').eq_iff

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