restrictScalars_injective — Mathlib

English

Restriction of scalars for algebraic equivalences is injective: if restrictScalars R f = restrictScalars R g then f = g.

Русский

Ограничение скаляров для алгебрав эквивалентностей инъективно: restrictScalars R f = restrictScalars R g ⇒ f = g.

LaTeX

$$$\text{restrictScalars}_R : (A \simeq_{{S}} B) \to (A \simeq_{{R}} B)$ is injective$$

Lean4

theorem restrictScalars_injective : Function.Injective (restrictScalars R : (A ≃ₐ[S] B) → A ≃ₐ[R] B) := fun _ _ h =>
  AlgEquiv.ext (AlgEquiv.congr_fun h :)

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