equal
deleted
inserted
replaced
754 proof (induct n) |
754 proof (induct n) |
755 case 0 |
755 case 0 |
756 show ?case by simp |
756 show ?case by simp |
757 next |
757 next |
758 case (Suc n) |
758 case (Suc n) |
759 then show ?case by (simp add: ring_eq_simps) |
759 then show ?case by (simp add: ring_simps) |
760 qed |
760 qed |
761 |
761 |
762 theorem arith_series_general: |
762 theorem arith_series_general: |
763 "((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
763 "((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = |
764 of_nat n * (a + (a + of_nat(n - 1)*d))" |
764 of_nat n * (a + (a + of_nat(n - 1)*d))" |