Commit 2025-01-17 18:44 80283e82

View on Github →

feat: define bases of root pairings (#20667)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/RootSystem/Base.lean

added theorem RootPairing.Base.coroot_mem_span_int

added theorem RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem

added theorem RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux

added theorem RootPairing.Base.exists_coroot_eq_sum_int

added theorem RootPairing.Base.exists_root_eq_sum_int

added theorem RootPairing.Base.exists_root_eq_sum_nat_or_neg

added theorem RootPairing.Base.root_mem_span_int

added theorem RootPairing.Base.span_coroot_support

added theorem RootPairing.Base.span_int_coroot_support

added theorem RootPairing.Base.span_int_root_support

added theorem RootPairing.Base.span_root_support

added def RootPairing.Base.toCoweightBasis

added def RootPairing.Base.toWeightBasis

added structure RootPairing.Base

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.coroot_eq_smul_coroot_iff

added def RootPairing.flipEquiv

added theorem RootPairing.smul_coroot_eq_of_root_eq_smul

added def RootSystem.flipEquiv