Theorems · Theorem · linear algebra

Submodule.toLinearPMap_graph_eq

∀ {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] [inst_4 : Module R F] (g : Submodule R (E × F)),
  (∀ x ∈ g, x.1 = 0 → x.2 = 0) → g.toLinearPMap.graph = g

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

4 results in Mathlib

Foundations

Depth 36 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingAddCommGroupModuleAddCommGroupModule