Theorem: RuesZ0Equals1 (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
⊢ Rues n 0 = 1
Tactic:
rw [RuesNEqualsExpSum]
State after:
n : ℕ+
⊢ (∑ m ∈ range ↑n, cexp (0 * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n = 1

State before:
n : ℕ+
⊢ (∑ m ∈ range ↑n, cexp (0 * cexp (2 * ↑π * (↑m / ↑↑n) * I))) / ↑↑n = 1
Tactic:
simp only [zero_mul, Complex.exp_zero, sum_const, card_range, nsmul_eq_mul, mul_one, ne_eq,
  Nat.cast_eq_zero, PNat.ne_zero, not_false_eq_true, div_self]
State after:
no goals