expand): golf a proof (#17428)

Commit

3 years ago

chore(data/polynomial/expand): golf a proof (#17428) Reuse the proof of `iff.mp` in `polynomial.expand_inj` to prove `polynomial.expand_injective`.

Author

urkud

Parents