Commit 2024-06-28 20:06 33d25d9a

View on Github →

refactor (LinearAlgebra/RootSystem) : change definition of RootPairing (#13917) We change the definition of RootPairing so that the induced reflection permutations on roots are required by definition to agree with those on coroots. This rules out pathologies, e.g., for infinite root systems.

Estimated changes

Modified Mathlib/LinearAlgebra/Reflection.lean

added theorem Module.bijOn_reflection_of_mapsTo

added theorem Module.eq_of_mapsTo_reflection_of_mem

added theorem Module.injOn_dualMap_subtype_span_range_range

added theorem Module.invOn_reflection_of_mapsTo

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

deleted theorem RootPairing.IsOrthogonal.symm

deleted theorem RootPairing.IsOrthogonal_comm

deleted theorem RootPairing.bijOn_coreflection_coroot

deleted theorem RootPairing.bijOn_reflection_root

deleted theorem RootPairing.coreflection_apply

deleted theorem RootPairing.coreflection_apply_self

deleted theorem RootPairing.coreflection_eq_flip_reflection

deleted theorem RootPairing.coreflection_image_eq

deleted theorem RootPairing.coreflection_invOn_self

deleted theorem RootPairing.coreflection_self

deleted theorem RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top'

deleted theorem RootPairing.coroot_eq_coreflection_of_root_eq_of_span_eq_top

deleted theorem RootPairing.coroot_root_eq_pairing

deleted theorem RootPairing.coroot_root_two

deleted theorem RootPairing.coxeterWeight_swap

deleted theorem RootPairing.eq_of_pairing_pairing_eq_two

deleted theorem RootPairing.flip_flip

deleted theorem RootPairing.isCrystallographic_iff

deleted theorem RootPairing.isReduced_iff

added def RootPairing.mk'

deleted theorem RootPairing.ne_zero'

deleted theorem RootPairing.ne_zero

deleted theorem RootPairing.pairing_same

deleted theorem RootPairing.reflection_apply

deleted theorem RootPairing.reflection_apply_root

deleted theorem RootPairing.reflection_apply_self

deleted theorem RootPairing.reflection_dualMap_eq_coreflection

deleted theorem RootPairing.reflection_image_eq

deleted theorem RootPairing.reflection_invOn_self

deleted theorem RootPairing.reflection_mul

deleted theorem RootPairing.reflection_same

deleted theorem RootPairing.root_coroot_eq_pairing

deleted theorem RootPairing.root_ne

deleted theorem RootSystem.coroot_eq_coreflection_of_root_eq

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.IsOrthogonal.symm

added theorem RootPairing.bijOn_coreflection_coroot

added theorem RootPairing.bijOn_reflection_root

added theorem RootPairing.coreflection_apply

added theorem RootPairing.coreflection_apply_coroot

added theorem RootPairing.coreflection_apply_self

added theorem RootPairing.coreflection_eq_flip_reflection

added theorem RootPairing.coreflection_image_eq

added theorem RootPairing.coreflection_same

added theorem RootPairing.coroot_eq_coreflection_of_root_eq

added theorem RootPairing.coroot_reflection_perm

added theorem RootPairing.coroot_root_eq_pairing

added theorem RootPairing.coroot_root_two

added theorem RootPairing.coxeterWeight_swap

added theorem RootPairing.flip_flip

added theorem RootPairing.isCrystallographic_iff

added theorem RootPairing.isOrthogonal_comm

added theorem RootPairing.isReduced_iff

added theorem RootPairing.mapsTo_coreflection_coroot

added theorem RootPairing.mapsTo_reflection_root

added theorem RootPairing.ne_zero'

added theorem RootPairing.ne_zero

modified def RootPairing.pairing

added theorem RootPairing.pairing_same

added theorem RootPairing.reflection_apply

added theorem RootPairing.reflection_apply_root

added theorem RootPairing.reflection_apply_self

added theorem RootPairing.reflection_dualMap_eq_coreflection

added theorem RootPairing.reflection_image_eq

added theorem RootPairing.reflection_same

added theorem RootPairing.root_coroot_eq_pairing

added theorem RootPairing.root_reflection_perm