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