`sumFirst_eq_zero_of_all_false`

proved

show as: view math explainer →

module: IndisputableMonolith.Streams
domain: Streams
line: 115 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Streams on GitHub at line 115.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 112  · norm_num
 113  · norm_num
 114
 115lemma sumFirst_eq_zero_of_all_false {m : Nat} {s : Stream}
 116  (h : ∀ i : Fin m, s i.val = false) :
 117  sumFirst m s = 0 := by
 118  unfold sumFirst
 119  have : (fun i : Fin m => (if s i.val then 1 else 0)) = (fun _ => 0) := by
 120    funext i; simp [h i]
 121  simp [this]
 122
 123end Streams
 124
 125end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.