restrictScalars_injective — Mathlib

English

The map that sends a S-subalgebra U to its restricted R-subalgebra is injective: distinct U give distinct restricted subalgebras.

Русский

Отображение U ↦ restrictScalars(R,U) инъективно: различные U дают различные ограниченные подалгебры.

LaTeX

$$Injective (restrictScalars R : Subalgebra S A → Subalgebra R A)$$

Lean4

theorem restrictScalars_injective : Function.Injective (restrictScalars R : Subalgebra S A → Subalgebra R A) :=
  fun U V H ↦ ext fun x ↦ by rw [← mem_restrictScalars R, H, mem_restrictScalars]

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