feat(algebra/group/defs): Division monoids (#13860)
Introduce what I call division monoids. Those are monoids `α` with a pseudo-inverse `⁻¹ : α → α ` and a pseudo-division `/ : α → α → α` respecting:
* `a / b = a * b⁻¹`
* `a⁻¹⁻¹ = a`
* `(a * b)⁻¹ = b⁻¹ * a⁻¹`
* `a * b = 1 → a⁻¹ = b`
This made-up algebraic structure has two uses:
* Deduplicate lemmas between `group` and `group_with_zero`. Almost all lemmas which are literally duplicated (same conclusion, same assumptions except for `group` vs `group_with_zero`) generalize to division monoids.
* Give access to lemmas for pointwise operations: `set α`, `finset α`, `filter α`, `submonoid α`, `subgroup α`, etc... all are division monoids when `α` is. In some sense, they are very close to being groups, the only obstruction being that `s / s ≠ 1` in general. Hence any identity which is true in a group/group with zero is also true in those pointwise monoids, if no cancellation is involved.
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
