Eric Wieser (Dec 03 2020 at 10:17):
We now have docs#alternating_map structures in mathlib, which are defined as being equal to zero when two inputs are zero.
However, the lemma docs#alternating_map.map_eq_zero_if_eq takes a bunch of hypotheses (
i ne j,
v i = v j), which I'm under the impression means it shouldn't be a simp lemma.
Is there any way to state a simp lemma without these hypotheses that would match and simplify
f ![a, b, a]?
Reid Barton (Dec 03 2020 at 10:24):
simp doesn't seem like the right tool for this
Reid Barton (Dec 03 2020 at 10:25):
In practice you probably don't have an explicit list of more than three arguments so just listing the 4 possible lemmas seems fine
Last updated: May 16 2021 at 05:21 UTC