restrictScalars_injective — Mathlib

English

The map restrictScalars is injective: if two S-linear equivalences become equal after restriction to R, then they were equal to begin with.

Русский

Отображение restrictScalars инъективно: если две S-эквивалентности становятся равными после ограничения к R, то они были равны изначально.

LaTeX

$$$\\text{restrictScalars\_injective} : \\forall f,g,\\ restrictScalars(R)(f) = \\restrictScalars(R)(g) \\Rightarrow f = g$$$

Lean4

theorem restrictScalars_injective : Function.Injective (restrictScalars R : (M ≃ₗ[S] M₂) → M ≃ₗ[R] M₂) := fun _ _ h ↦
  ext (LinearEquiv.congr_fun h :)

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