Theorem RootPairing.root_add_root_mem_of_pairingIn_neg

Modification history

2025-07-04 07:44
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
chore: further whitespace fixes (#26708) …
Modified RootPairing.root_add_root_mem_of_pairingIn_negView on Github →
2025-02-26 10:06
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
feat: more structural lemmas about root pairings (#22213) …
Modified RootPairing.root_add_root_mem_of_pairingIn_negView on Github →
2025-02-21 21:53
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
feat: basic structural lemmas about finite crystallographic root pairings. (#21932)
Added RootPairing.root_add_root_mem_of_pairingIn_negView on Github →