Commit 2025-05-28 22:04 78ab2f60

View on Github →

chore: rename reflection_perm to reflectionPerm (#25275) This matches the naming convention.

Estimated changes

Modified Mathlib/LinearAlgebra/RootSystem/BaseChange.lean

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

added theorem RootPairing.chainBotCoeff_reflectionPerm_left

added theorem RootPairing.chainBotCoeff_reflectionPerm_right

deleted theorem RootPairing.chainBotCoeff_reflection_perm_left

deleted theorem RootPairing.chainBotCoeff_reflection_perm_right

added theorem RootPairing.chainTopCoeff_reflectionPerm_left

added theorem RootPairing.chainTopCoeff_reflectionPerm_right

deleted theorem RootPairing.chainTopCoeff_reflection_perm_left

deleted theorem RootPairing.chainTopCoeff_reflection_perm_right

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.coroot'_reflectionPerm

deleted theorem RootPairing.coroot'_reflection_perm

added theorem RootPairing.coroot_reflectionPerm

deleted theorem RootPairing.coroot_reflection_perm

added theorem RootPairing.isFixedPt_reflectionPerm_iff

deleted theorem RootPairing.isFixedPt_reflection_perm_iff

added theorem RootPairing.pairing_reflectionPerm

added theorem RootPairing.pairing_reflectionPerm_self_left

added theorem RootPairing.pairing_reflectionPerm_self_right

deleted theorem RootPairing.pairing_reflection_perm

deleted theorem RootPairing.pairing_reflection_perm_self_left

deleted theorem RootPairing.pairing_reflection_perm_self_right

modified theorem RootPairing.pairing_smul_coroot_eq

modified theorem RootPairing.pairing_smul_root_eq

added theorem RootPairing.reflectionPerm_eq_iff_smul_coroot

added theorem RootPairing.reflectionPerm_eq_iff_smul_root

added theorem RootPairing.reflectionPerm_eq_of_pairing_eq_zero'

added theorem RootPairing.reflectionPerm_eq_of_pairing_eq_zero

added theorem RootPairing.reflectionPerm_eq_reflectionPerm_iff_of_isSMulRegular

added theorem RootPairing.reflectionPerm_eq_reflectionPerm_iff_of_span

added theorem RootPairing.reflectionPerm_inv

added theorem RootPairing.reflectionPerm_involutive

added theorem RootPairing.reflectionPerm_self

added theorem RootPairing.reflectionPerm_sq

added theorem RootPairing.reflectionPerm_symm

deleted theorem RootPairing.reflection_perm_eq_iff_smul_coroot

deleted theorem RootPairing.reflection_perm_eq_iff_smul_root

deleted theorem RootPairing.reflection_perm_eq_of_pairing_eq_zero'

deleted theorem RootPairing.reflection_perm_eq_of_pairing_eq_zero

deleted theorem RootPairing.reflection_perm_eq_reflection_perm_iff_of_isSMulRegular

deleted theorem RootPairing.reflection_perm_eq_reflection_perm_iff_of_span

deleted theorem RootPairing.reflection_perm_inv

deleted theorem RootPairing.reflection_perm_involutive

deleted theorem RootPairing.reflection_perm_self

deleted theorem RootPairing.reflection_perm_sq

deleted theorem RootPairing.reflection_perm_symm

modified theorem RootPairing.reflection_sq

added theorem RootPairing.root_reflectionPerm

deleted theorem RootPairing.root_reflection_perm

modified theorem RootPairing.two_nsmul_reflection_eq_of_perm_eq

added theorem RootSystem.reflectionPerm_eq_reflectionPerm_iff

deleted theorem RootSystem.reflection_perm_eq_reflection_perm_iff

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean

modified def RootPairing.EmbeddedG2.shortAddLong

modified def RootPairing.EmbeddedG2.threeShortAddLong

modified def RootPairing.EmbeddedG2.threeShortAddTwoLong

modified def RootPairing.EmbeddedG2.twoShortAddLong

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

Modified Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean

added theorem RootPairing.corootSpanMem_reflectionPerm_self

deleted theorem RootPairing.corootSpanMem_reflection_perm_self

added theorem RootPairing.pairingIn_reflectionPerm

added theorem RootPairing.pairingIn_reflectionPerm_self_left

added theorem RootPairing.pairingIn_reflectionPerm_self_right

deleted theorem RootPairing.pairingIn_reflection_perm

deleted theorem RootPairing.pairingIn_reflection_perm_self_left

deleted theorem RootPairing.pairingIn_reflection_perm_self_right

added theorem RootPairing.rootSpanMem_reflectionPerm_self

deleted theorem RootPairing.rootSpanMem_reflection_perm_self

Modified Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean

added theorem RootPairing.RootPositiveForm.rootLength_reflectionPerm_self

deleted theorem RootPairing.RootPositiveForm.rootLength_reflection_perm_self

Modified Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean