Theorems · Theorem · group theory

LinearEquiv.fixedSubmodule_transvection_mul

∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] (e : V ≃ₗ[K] V) {f : Module.Dual K V} {v : V},
  v ∉ (↑e).fixedSubmodule →
    Submodule.map f (↑e).fixedSubmodule = ⊥ →
      ∀ (hfv : f (v - e v) = 0),
        f (e v) = 1 → (↑(LinearEquiv.transvection hfv * e)).fixedSubmodule = (↑e).fixedSubmodule ⊔ K ∙ v

Defined in

Mathlib.LinearAlgebra.Transvection.Generation

Cited by

0 results in Mathlib

Foundations

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

Assumes

DivisionRingAddCommGroupModuleModule.Finite