mathlib

918e5d82 - chore(data/finsupp): replace `eq_zero_of_zero_eq_one` with `finsupp.unique_of_right` (#4563)

chore(data/finsupp): replace `eq_zero_of_zero_eq_one` with `finsupp.unique_of_right` (#4563) Also add a lemma `semimodule.subsingleton`: if `R` is a subsingleton semiring, then any semimodule over `R` is a subsingleton.