Commit 2025-08-11 09:25 16d91fe7

View on Github →

feat: drop assumption [P.IsNotG2] in lemma RootPairing.lie_e_f_ne (#28011) We also move a few lemmas from LinearAlgebra.RootSystem.Chain into LinearAlgebra.RootSystem.Finite.G2 so that we can invert the import order of these two files. The motivation for this is to allow us to import LinearAlgebra.RootSystem.Base into LinearAlgebra.RootSystem.Finite.G2.

Estimated changes

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

deleted theorem RootPairing.chainBotCoeff_add_chainTopCoeff_le_two

deleted theorem RootPairing.chainBotCoeff_if_one_zero

deleted theorem RootPairing.chainTopCoeff_if_one_zero

deleted theorem RootPairing.pairingIn_le_zero_of_root_add_mem

deleted theorem RootPairing.zero_le_pairingIn_of_root_sub_mem

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.pairing_eq_add_of_root_eq_smul_add_smul

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

added def RootPairing.EmbeddedG2.basis

added theorem RootPairing.IsG2.card_base_support_eq_two

added theorem RootPairing.IsG2.nonempty

added theorem RootPairing.IsG2.span_eq_rootSpan_int

added def RootPairing.IsG2.toEmbeddedG2

added theorem RootPairing.chainBotCoeff_add_chainTopCoeff_le_two

added theorem RootPairing.chainBotCoeff_if_one_zero

added theorem RootPairing.chainTopCoeff_if_one_zero

added theorem RootPairing.pairingIn_le_zero_of_root_add_mem

added theorem RootPairing.zero_le_pairingIn_of_root_sub_mem

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean

modified theorem RootPairing.GeckConstruction.lie_e_f_ne

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean

added theorem RootPairing.chainBotCoeff_mul_chainTopCoeff.isNotG2

Modified Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean

added theorem RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul