restrictScalars_trans — Mathlib

English

Restriction of scalars is transitive: restricting from S to R via an intermediate type T yields the same as restricting directly to R: (f.restrictScalars S).restrictScalars R = f.restrictScalars R.

Русский

Ограничение скаляров транзитивно: ограничение через промежуточный слой S → T → R равно прямому ограничению к R: (f.restrictScalars S).restrictScalars R = f.restrictScalars R.

LaTeX

$$$ (f|_{S})|_{R} = f|_{R} $$$

Lean4

@[simp]
theorem restrictScalars_trans {T : Type*} [Semiring T] [Module T M] [Module T N] [CompatibleSMul M N S T]
    [CompatibleSMul M N R T] (f : M →ₗ[T] N) : (f.restrictScalars S).restrictScalars R = f.restrictScalars R :=
  rfl

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