Commit 2025-07-08 08:42 1aa6f29d

View on Github →

feat: add induction principle for positive roots relative to a base of a root system (#26819)

Estimated changes

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

added theorem RootPairing.Base.IsPos.add

added theorem RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn

added theorem RootPairing.Base.IsPos.induction_on

added theorem RootPairing.Base.IsPos.sub

added def RootPairing.Base.IsPos

added theorem RootPairing.Base.exists_eq_sum_and_forall_sum_mem_of_isPos

added theorem RootPairing.Base.pos_of_sum_smul_sub_mem_range_root

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

modified def RootPairing.GeckConstruction.cartanSubalgebra

modified def RootPairing.GeckConstruction.lieAlgebra

modified theorem RootPairing.GeckConstruction.lie_e_f_mul_ω

modified theorem RootPairing.GeckConstruction.ω_mul_e

modified theorem RootPairing.GeckConstruction.ω_mul_f

modified theorem RootPairing.GeckConstruction.ω_mul_h

modified theorem RootPairing.GeckConstruction.ω_mul_ω

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

added theorem RootPairing.nsmul_notMem_range_root

deleted theorem RootPairing.two_smul_notMem_range_root