Commit 2024-07-01 22:27 9bb64890

feat: add LinearMap.IsAlt.eq_of_add_add_eq_zero (#14281) For an alternating form $B : M \times M \to R$ and $a, b, c \in M$ with $a + b+ c = 0$, we have $B(a, b) = B(b, c)$. This can be used to prove the same property of Wronskian: see #14243.