of'_dvd_iff_modOf_eq_zero — Mathlib

English

Basis element divides x iff the remainder mod g is zero.

Русский

Базисный элемент делит x тогда и только тогда, когда остаток по g равен нулю.

LaTeX

$$$\\operatorname{of}'(g) \\mid x \\quad\\text{iff}\\quad x \\bmod^{\\circ} g = 0$$$

Lean4

theorem of'_dvd_iff_modOf_eq_zero [IsCancelAdd G] {x : k[G]} {g : G} : of' k G g ∣ x ↔ x %ᵒᶠ g = 0 :=
  by
  constructor
  · rintro ⟨x, rfl⟩
    rw [of'_mul_modOf]
  · intro h
    rw [← divOf_add_modOf x g, h, add_zero]
    exact dvd_mul_right _ _

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