Commit 2024-10-02 22:35 655d653b

View on Github →

feat (LinearAlgebra/RootPairing/Finite) : The canonical bilinear form on a finite root pairing (#17070) This PR introduces the canonical bilinear form for a finite root pairing, and proves some basic properties.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Ring/SumsOfSquares.lean

added theorem isSumSq_sum_mul_self

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.coroot'_reflection

added theorem RootPairing.coroot'_reflection_perm

modified def RootPairing.pairing

added theorem RootPairing.pairing_reflection_perm

added theorem RootPairing.pairing_reflection_perm_self_left

added theorem RootPairing.pairing_reflection_perm_self_right

added theorem RootPairing.root'_coroot_eq_pairing

added theorem RootPairing.root_coroot'_eq_pairing

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

added def RootPairing.CoPolarization

added theorem RootPairing.CoPolarization_apply

added theorem RootPairing.CoPolarization_eq

added def RootPairing.CorootForm

added def RootPairing.Polarization

added theorem RootPairing.Polarization_apply

added def RootPairing.RootForm

added theorem RootPairing.corootForm_self_smul_root

added theorem RootPairing.rootForm_apply_apply

added theorem RootPairing.rootForm_reflection_reflection_apply

added theorem RootPairing.rootForm_root_self

added theorem RootPairing.rootForm_self_smul_coroot

added theorem RootPairing.rootForm_self_sum_of_squares

added theorem RootPairing.rootForm_symmetric

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean