divOf_add_modOf — Mathlib

English

Division algorithm holds: x equals the product by the quotient plus the remainder.

Русский

Деление по модулю: x равно произведению частного на делитель плюс остаток.

LaTeX

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

Lean4

theorem divOf_add_modOf [IsCancelAdd G] (x : k[G]) (g : G) : of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x :=
  by
  ext g'
  rw [Finsupp.add_apply]
  obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)
  swap
  · rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h, zero_add]
  · rw [modOf_apply_self_add, add_zero]
    rw [of'_apply, single_mul_apply_aux, one_mul, divOf_apply]
    intro a ha
    exact add_right_inj _

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