Theorems · Theorem · linear algebra

LinearMap.exists_extend_of_notMem

∀ {K : Type u_3} {V : Type u_4} {V' : Type u_5} [inst : DivisionRing K] [inst_1 : AddCommGroup V]
  [inst_2 : AddCommGroup V'] [inst_3 : Module K V] [inst_4 : Module K V'] {p : Submodule K V} {v : V} (f : ↥p →ₗ[K] V'),
  v ∉ p → ∀ (y : V'), ∃ g, g ∘ₗ p.subtype = f ∧ g v = y

Defined in

Mathlib.LinearAlgebra.Basis.VectorSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupAddCommGroupModuleModule