Commit 2024-07-30 02:04 31b40b49

feat (LinearAlgebra/RootSystem/RootPositive) : Root-positive bilinear forms (#15155) This PR introduces a Prop-valued mixin class for root pairings, specifying that a bilinear form on weight space is symmetric, reflection-invariant, and gives roots a strictly positive norm. Given a root-positive norm, one obtains sign-compatibilities between the form and the canonical pairing between roots and coroots. Root-positive forms show up naturally in Kac-Moody Lie algebras (without the name), and the canonical polarization on a finite root pairing induces a root-positive form.