mathlib3

3711afe1 - feat(ring_theory/non_unital_subsemiring/basic): introduce non-unital subsemirings and develop basic API (#13749)

feat(ring_theory/non_unital_subsemiring/basic): introduce non-unital subsemirings and develop basic API (#13749) - [x] depends on: #13627 - [x] depends on: #13747 - [x] depends on: #13748 - [x] depends on: #13945 - [x] depends on: #13958