Theorem RootPairing.toLinearMap_eq_toPerfectPairing

Modification history

2026-01-15 12:34
Mathlib/LinearAlgebra/RootSystem/Defs.lean
chore: remove declarations deprecated between 2021-01-15 and 2025-07-15 (#33988) …
Deleted RootPairing.toLinearMap_eq_toPerfectPairingView on Github →
2025-04-23 04:28
Mathlib/LinearAlgebra/RootSystem/Defs.lean
refactor(PerfectPairing): rename the structure fields (#24231) …
Added RootPairing.toLinearMap_eq_toPerfectPairingView on Github →