case mp
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0

case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ of' k G g ∣ x ↔ x %ᵒᶠ g = 0
constructor
case mp.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
⊢ of' k G g * x %ᵒᶠ g = 0
case mp
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ of' k G g ∣ x → x %ᵒᶠ g = 0
rintro ⟨x, rfl⟩
no goals
case mp.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
g : G
x : AddMonoidAlgebra k G
⊢ of' k G g * x %ᵒᶠ g = 0
rw [of'_mul_modOf]
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
⊢ x %ᵒᶠ g = 0 → of' k G g ∣ x
intro h
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ x
rw [← divOf_add_modOf x g, h, add_zero]
no goals
case mpr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : AddMonoidAlgebra k G
g : G
h : x %ᵒᶠ g = 0
⊢ of' k G g ∣ of' k G g * (x /ᵒᶠ g)
exact dvd_mul_right _ _