Theorem RootPairing.zero_lt_pairingIn_iff'

Modification history

2025-05-01 22:01

Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

feat: add supporting API for Geck's final root system lemma (#24476) …

Modified RootPairing.zero_lt_pairingIn_iff'View on Github →

2025-02-26 10:06

Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

feat: more structural lemmas about root pairings (#22213) …

Added RootPairing.zero_lt_pairingIn_iff'View on Github →