Commit 2023-02-28 10:55 a51ce549
View on Github →chore(data/set/semiring): add an idem_semiring instance (#18449)
This typeclass is reasonably new, so some obvious instances are missing.
Also adds some basic API lemmas that were missing about the casting functions set.up and set_semiring.down.
forward-ported as https://github.com/leanprover-community/mathlib4/pull/2518