Theorems · Theorem · linear algebra

LinearPMap.mkSpanSingleton_apply

∀ (K : Type u_7) (L : Type u_8) {E : Type u_9} {F : Type u_10} [inst : DivisionRing K] [inst_1 : DivisionRing L]
  {σ : K →+* L} [inst_2 : AddCommGroup E] [inst_3 : Module K E] [inst_4 : AddCommGroup F] [inst_5 : Module L F] {x : E}
  (hx : x ≠ 0) (y : F), ↑(LinearPMap.mkSpanSingleton x y hx) ⟨x, ⋯⟩ = y

Defined in

Mathlib.LinearAlgebra.LinearPMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRingDivisionRingAddCommGroupModuleAddCommGroupModule