Commit 2025-09-01 12:03 035d719c

feat: a root system is determined by its Cartan matrix (#29052) Moving the lemma RootPairing.InvariantForm.apply_weylGroup_smul allows us to drop an import in Mathlib.LinearAlgebra.RootSystem.RootPositive and thus to import Mathlib.LinearAlgebra.RootSystem.Basic in Mathlib.LinearAlgebra.RootSystem.Hom. This is necessary to make the key lemma RootSystem.ext available for the proof of RootPairing.Equiv.mk'.