Theorems · Theorem · linear algebra

LinearMap.BilinForm.dualSubmodule_span_of_basis

∀ {R : Type u_4} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) {ι : Type u_1} [inst_7 : Finite ι] [inst_8 : DecidableEq ι] (hB : B.Nondegenerate)
  (b : Module.Basis ι S M),
  B.dualSubmodule (Submodule.span R (Set.range ⇑b)) = Submodule.span R (Set.range ⇑(B.dualBasis hB b))

Defined in

Mathlib.LinearAlgebra.BilinearForm.DualLattice

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingFieldAddCommGroupAlgebraModuleModuleIsScalarTowerFiniteDecidableEq