mathlib

669a3499 - feat(data/prod): mk injective lemmas (#4319)

feat(data/prod): mk injective lemmas (#4319) More scattered lemmmas from the Witt vector branch. Co-authored by: Johan Commelin <johan@commelin.net> Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>