Def RootSystem.mk'

Modification history

2025-12-15 09:35
Mathlib/LinearAlgebra/RootSystem/Basic.lean
refactor: turn `RootSystem` into a mixin rather than extending `RootPairing` (#32885) …
Deleted RootSystem.mk'View on Github →
2025-01-09 09:30
Mathlib/LinearAlgebra/RootSystem/Basic.lean
feat: make spanning condition in `RootSystem` symmetric for roots and coroots. (#20564) …
Modified RootSystem.mk'View on Github →
2023-12-13 17:01
Mathlib/LinearAlgebra/RootSystem/Basic.lean
feat: define root data / systems (#8882)
Added RootSystem.mk'View on Github →