Lean4
instance commSemiring : CommSemiring Num where
__ := Num.addMonoid
__ := Num.addMonoidWithOne
mul := (· * ·)
npow := @npowRec Num ⟨1⟩ ⟨(· * ·)⟩
mul_zero _ := by rw [← to_nat_inj, mul_to_nat, cast_zero, mul_zero]
zero_mul _ := by rw [← to_nat_inj, mul_to_nat, cast_zero, zero_mul]
mul_one _ := by rw [← to_nat_inj, mul_to_nat, cast_one, mul_one]
one_mul _ := by rw [← to_nat_inj, mul_to_nat, cast_one, one_mul]
add_comm _ _ := by simp_rw [← to_nat_inj, add_to_nat, add_comm]
mul_comm _ _ := by simp_rw [← to_nat_inj, mul_to_nat, mul_comm]
mul_assoc _ _ _ := by simp_rw [← to_nat_inj, mul_to_nat, mul_assoc]
left_distrib _ _ _ := by simp only [← to_nat_inj, mul_to_nat, add_to_nat, mul_add]
right_distrib _ _ _ := by simp only [← to_nat_inj, mul_to_nat, add_to_nat, add_mul]
