Commit 2025-04-23 04:28 9f2b5fe4

View on Github →

refactor(PerfectPairing): rename the structure fields (#24231) That way, they match the naming convention. From Toric

Estimated changes

Modified Mathlib/Algebra/Lie/Weights/RootSystem.lean

Modified Mathlib/LinearAlgebra/PerfectPairing/Basic.lean

deleted theorem PerfectPairing.toLin_apply

added theorem PerfectPairing.toLinearMap_apply

modified structure PerfectPairing

Modified Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

modified def PerfectPairing.restrict

Modified Mathlib/LinearAlgebra/RootSystem/BaseChange.lean

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

modified theorem RootPairing.coroot_root_eq_pairing

deleted theorem RootPairing.toLin_toPerfectPairing

added theorem RootPairing.toLinearMap_eq_toPerfectPairing

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

Modified Mathlib/LinearAlgebra/RootSystem/Hom.lean

Modified Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean