mathlib
ca7347c4 - refactor(ring_theory/sub[semi]ring): move pointwise instances to their own file (#10347)

Commit
4 years ago
refactor(ring_theory/sub[semi]ring): move pointwise instances to their own file (#10347) This matches how we have separate pointwise files for `submonoid` and `subgroup`. All the new lemmas are direct copies of the subgroup lemmas.
Author
Parents
Loading