Lean4
instance : CommRing (Poly α) where
__ := (inferInstance : AddCommGroup (Poly α))
__ := (inferInstance : AddGroupWithOne (Poly α))
mul := (· * ·)
npow := @npowRec _ ⟨(1 : Poly α)⟩ ⟨(· * ·)⟩
mul_zero _ := by ext; rw [mul_apply, zero_apply, mul_zero]
zero_mul _ := by ext; rw [mul_apply, zero_apply, zero_mul]
mul_one _ := by ext; rw [mul_apply, one_apply, mul_one]
one_mul _ := by ext; rw [mul_apply, one_apply, one_mul]
mul_comm _ _ := by ext; simp_rw [mul_apply, mul_comm]
mul_assoc _ _ _ := by ext; simp_rw [mul_apply, mul_assoc]
left_distrib _ _ _ := by ext; simp_rw [add_apply, mul_apply]; apply mul_add
right_distrib _ _ _ := by ext; simp only [add_apply, mul_apply]; apply add_mul
