Commit 2023-12-13 17:01 3e7a07fa

View on Github →

feat: define root data / systems (#8882)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/PerfectPairing.lean

added def IsReflexive.toPerfectPairingDual

added theorem PerfectPairing.flip_flip

added structure PerfectPairing

Created Mathlib/LinearAlgebra/RootSystem/Basic.lean

added def RootPairing.IsCrystallographic

added def RootPairing.IsReduced

added theorem RootPairing.bijOn_coreflection_coroot

added theorem RootPairing.bijOn_reflection_root

added def RootPairing.coreflection

added theorem RootPairing.coreflection_apply

added theorem RootPairing.coreflection_image_eq

added theorem RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top'

added theorem RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top

added theorem RootPairing.coroot_root_two

added theorem RootPairing.eq_of_forall_coroot_root_eq

added theorem RootPairing.flip_flip

added theorem RootPairing.injOn_dualMap_subtype_span_root_coroot

added theorem RootPairing.ne_zero'

added theorem RootPairing.ne_zero

added def RootPairing.reflection

added theorem RootPairing.reflection_apply

added theorem RootPairing.reflection_apply_self

added theorem RootPairing.reflection_dualMap_eq_coreflection

added theorem RootPairing.reflection_image_eq

added structure RootPairing

added theorem RootSystem.coroot_eq_coreflection_of_root_eq

added def RootSystem.mk'

added structure RootSystem