English
Let α be a monoid and a ∈ α. For any unit u ∈ Units α, define a divided by u as a · u^{-1}. This operation is defined only when the second argument is invertible and is not totalized at zero.
Русский
Пусть α — моноид и a ∈ α. Для любого единичного элемента u ∈ Units α задаётся частичное деление a /ₚ u = a · u^{-1}. Эта операция определяется только для обратимого второго аргумента и не является тотальной по отношению к нулю.
LaTeX
$$$a /ₚ u = a \cdot u^{-1}$$$
Lean4
/-- Partial division, denoted `a /ₚ u`. It is defined when the
second argument is invertible, and unlike the division operator
in `DivisionRing` it is not totalized at zero. -/
def divp (a : α) (u : Units α) : α :=
a * (u⁻¹ : αˣ)
