Documentation
RootSystem
.
Cn
Search
return to top
source
Imports
Aesop
Init
Mathlib.Tactic.Cases
Mathlib.Tactic.Ext
Mathlib.Tactic.Linarith
Mathlib.Tactic.NormNum
Mathlib.Tactic.Ring
Mathlib.Tactic.Tauto
Mathlib.LinearAlgebra.RootSystem.Defs
Mathlib.LinearAlgebra.RootSystem.Irreducible
Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Mathlib.LinearAlgebra.RootSystem.Reduced
Mathlib.Order.Interval.Finset.Fin
Imported by