Commit 2024-11-20 20:34 3c79dac7

View on Github →

feat (LinearAlgebra/RootSystem/Finite): nondegeneracy of canonical bilinear form restricted to root span (#18569) The canonical bilinear form for a root pairing over a linearly ordered commutative ring is nondegenerate when restricted to the span of roots.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

added theorem Finset.sum_mul_self_eq_zero_iff

Modified Mathlib/LinearAlgebra/Dimension/Basic.lean

added theorem rank_le_of_smul_regular

Modified Mathlib/LinearAlgebra/Dimension/RankNullity.lean

added theorem Submodule.disjoint_ker_of_finrank_eq

Modified Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean

added theorem LinearMap.finrank_le_of_smul_regular

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

added theorem RootPairing.prod_rootForm_root_self_pos

added theorem RootPairing.prod_rootForm_smul_coroot_mem_range_domRestrict

added theorem RootPairing.range_polarization_domRestrict_le_span_coroot

added theorem RootPairing.rootForm_root_self_pos

added theorem RootPairing.rootForm_self_non_neg

added theorem RootPairing.rootForm_self_zero_iff

Created Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

added theorem RootPairing.disjoint_rootSpan_ker_polarization

added theorem RootPairing.eq_zero_of_mem_rootSpan_of_rootForm_self_eq_zero

added theorem RootPairing.finrank_corootSpan_eq

added theorem RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan

added theorem RootPairing.mem_ker_polarization_of_rootForm_self_eq_zero

added theorem RootPairing.rootForm_pos_of_nonzero

added theorem RootPairing.rootForm_restrict_nondegenerate

added theorem RootPairing.rootForm_rootPositive

added theorem RootSystem.rootForm_anisotropic

Modified docs/references.bib