Theorem RootPairing.Base.sub_nmem_range_root

Modification history

2025-05-25 12:30
Mathlib/LinearAlgebra/RootSystem/Base.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted RootPairing.Base.sub_nmem_range_rootView on Github →
2025-02-26 10:06
Mathlib/LinearAlgebra/RootSystem/Base.lean
feat: more structural lemmas about root pairings (#22213) …
Added RootPairing.Base.sub_nmem_range_rootView on Github →