Theorems · Theorem · ring theory

LinearMap.restrictScalars_trans

∀ {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module S M] [inst_7 : Module S N] [inst_8 : LinearMap.CompatibleSMul M N R S] {T : Type u_20}
  [inst_9 : Semiring T] [inst_10 : Module T M] [inst_11 : Module T N] [inst_12 : LinearMap.CompatibleSMul M N S T]
  [inst_13 : LinearMap.CompatibleSMul M N R T] (f : M →ₗ[T] N), ↑R (↑S f) = ↑R f

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

0 results in Mathlib

Foundations

Depth 25 from the axioms · uses no axioms

Assumes

SemiringSemiringAddCommMonoidAddCommMonoidModuleModuleModuleModuleLinearMap.CompatibleSMulSemiringModuleModuleLinearMap.CompatibleSMulLinearMap.CompatibleSMul