modOf_add_divOf — Mathlib

English

A symmetric form of the division algorithm: remainder plus basis times quotient equals x.

Русский

Симметричная форма деления: остаток плюс базис умноженный на частное равно x.

LaTeX

$$$ (x \\bmod^{\\circ} g) + \\operatorname{of}'(g) \\cdot (x /^{\\circ} g) = x $$$

Lean4

theorem modOf_add_divOf [IsCancelAdd G] (x : k[G]) (g : G) : x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x := by
  rw [add_comm, divOf_add_modOf]

Похожие утверждения