Commit 2022-11-08 14:54 9619aca9
View on Github →chore(data/polynomial/expand): golf a proof (#17428)
Reuse the proof of iff.mp in polynomial.expand_inj to prove polynomial.expand_injective.
chore(data/polynomial/expand): golf a proof (#17428)
Reuse the proof of iff.mp in polynomial.expand_inj to prove polynomial.expand_injective.