Theorem RootPairing.InvariantForm.exists_apply_eq_or_aux
Modification history
2025-08-15 16:30
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
chore: bump toolchain to v4.23.0-rc2 (#28454)
Deleted RootPairing.InvariantForm.exists_apply_eq_or_auxView on Github →2025-08-11 21:53
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
fix: revert several flaky grind golfs (#28272) …
Added RootPairing.InvariantForm.exists_apply_eq_or_auxView on Github →