Commit 2023-12-12 15:39 55d44371

View on Github →

feat: Define dual submodule wrt bilinear form (#8997)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Basic.lean

added theorem BilinForm.smul_left_of_tower

added theorem BilinForm.smul_right_of_tower

Created Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

added def BilinForm.dualSubmodule

added def BilinForm.dualSubmoduleParing

added theorem BilinForm.dualSubmoduleParing_spec

added def BilinForm.dualSubmoduleToDual

added theorem BilinForm.dualSubmoduleToDual_injective

added theorem BilinForm.dualSubmodule_dualSubmodule_flip_of_basis

added theorem BilinForm.dualSubmodule_dualSubmodule_of_basis

added theorem BilinForm.dualSubmodule_flip_dualSubmodule_of_basis

added theorem BilinForm.dualSubmodule_span_of_basis

added theorem BilinForm.le_flip_dualSubmodule

added theorem BilinForm.mem_dualSubmodule

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

added theorem BilinForm.Nondegenerate.flip

added theorem BilinForm.dualBasis_dualBasis

added theorem BilinForm.dualBasis_dualBasis_flip

added theorem BilinForm.dualBasis_flip_dualBasis

added theorem BilinForm.nonDegenerateFlip_iff