Commit 2026-02-24 20:40 e30ddc5f

View on Github →

feat(LinearAlgebra/QuadraticForm): radical of a quadratic form (#34493) Define the radical of a quadratic form, and show that its dimension is invariant under equivalences.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Basis/Basic.lean

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

added theorem Pi.dim_spanSubset

Modified Mathlib/LinearAlgebra/LinearIndependent/Defs.lean

added theorem LinearIndependent.linearIndepOn

deleted theorem linearIndepOn_univ

added theorem linearIndepOn_univ_iff

Modified Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

added theorem QuadraticMap.IsometryEquiv.apply_symm_apply

added theorem QuadraticMap.IsometryEquiv.coe_symm_toLinearEquiv

added theorem QuadraticMap.IsometryEquiv.symm_apply_apply

Created Mathlib/LinearAlgebra/QuadraticForm/Radical.lean

added theorem QuadraticForm.finrank_radical_of_equiv_weightedSumSquares

added theorem QuadraticForm.radical_weightedSumSquares

added theorem QuadraticMap.Equivalent.rank_radical_eq

added theorem QuadraticMap.IsometryEquiv.map_radical

added structure QuadraticMap.Nondegenerate

added theorem QuadraticMap.le_radical_iff

added theorem QuadraticMap.lift_mk

added theorem QuadraticMap.mem_radical_iff'

added theorem QuadraticMap.nondegenerate_associated_iff

added theorem QuadraticMap.nondegenerate_iff_radical_eq_bot

added theorem QuadraticMap.nondegenerate_polar_iff

added def QuadraticMap.radical

added theorem QuadraticMap.radical_eq_ker_associated

added theorem QuadraticMap.radical_eq_ker_polarBilin

added theorem QuadraticMap.radical_le_ker_polarBilin

Modified Mathlib/LinearAlgebra/StdBasis.lean

added theorem Pi.mem_spanSubset_iff

added def Pi.spanSubset

Modified docs/references.bib