Theorems · Theorem · linear algebra

LinearPMap.smul_graph

∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] {M : Type u_7} [inst_4 : Monoid M] [inst_5 : DistribMulAction M F] [inst_6 : Module R F]
  [inst_7 : SMulCommClass R M F] (f : E →ₗ.[R] F) (z : M),
  (z • f).graph = Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph

The graph of z • f as a pushforward.

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

0 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Quot.sound

Assumes

RingAddCommGroupModuleAddCommGroupMonoidDistribMulActionModuleSMulCommClass