Commit 2023-05-21 20:10 b2c89893

chore(data/multiset/pi): correct names and reorder (#19050)

• multiset.pi_cons_injective is about multiset.pi.cons so should have a . in its name.
• multiset.pi.cons_ext is not an ext lemma, but more closely resembles eta-reduction. This also groups together the lemmas about pi.cons.