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

deleted theorem RootPairing.flip_flip
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.root_ne