Commit 2022-05-05 23:51 151933d1

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.