Theorems · Theorem · group theory

LinearEquiv.sup_span_singleton_lt_top

∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {W : Submodule K V} (v : V), 1 < Module.finrank K (V ⧸ W) → W ⊔ K ∙ v < ⊤

Defined in

Mathlib.LinearAlgebra.Transvection.Generation

Cited by

1 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModuleModule.Finite