English
In a monoid with inverses, the division a ÷ b is defined as a b^{-1}.
Русский
В моноиде с обратимыми элементами деление a ÷ b определяется как a · b^{-1}.
LaTeX
$$$\\mathrm{div}'(a,b) = a \\cdot b^{-1}$$$
Lean4
/-- In a class equipped with instances of both `Monoid` and `Inv`, this definition records what the
default definition for `Div` would be: `a * b⁻¹`. This is later provided as the default value for
the `Div` instance in `DivInvMonoid`.
We keep it as a separate definition rather than inlining it in `DivInvMonoid` so that the `Div`
field of individual `DivInvMonoid`s constructed using that default value will not be unfolded at
`.instance` transparency. -/
def div' {G : Type u} [Monoid G] [Inv G] (a b : G) : G :=
a * b⁻¹
