LeanMachineLearning exposition

sum_mod_range🔗

Minimal Lean file

sum_mod_range🔗

Lemmasum_mod_range
Details

No docstring.

🔗theorem
sum_mod_range {K : ℕ} (hK : 0 < K) (a : Fin K) :
  (∑ s ∈ Finset.range K, if ⟨s % K, ⋯⟩ = a then 1 else 0) = 1
sum_mod_range {K : ℕ} (hK : 0 < K)
  (a : Fin K) :
  (∑ s ∈ Finset.range K,
      if ⟨s % K, ⋯⟩ = a then 1 else 0) =
    1

Code

lemma sum_mod_range {K : ℕ} (hK : 0 < K) (a : Fin K) :
    (∑ s ∈ range K, if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) = 1
Used by (1)

Actions: Source · Open Issue

Proof
by
  have h_iff (s : ℕ) (hs : s < K) : ⟨s % K, Nat.mod_lt _ hK⟩ = a ↔ s = a := by
    simp only [Nat.mod_eq_of_lt hs, Fin.ext_iff]
  calc (∑ s ∈ range K, if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0)
  _ = ∑ s ∈ range K, if s = a then 1 else 0 := sum_congr rfl fun s hs ↦ by grind
  _ = _ := by
    rw [sum_ite_eq']
    simp