mathlib4
mathlib4 copied to clipboard
feat: sorried ports of lemmas used by norm_num/ring
trafficstars
- [ ] depends on #470, for
OrderedRing.