theorem proved term proof

`rs_pattern_phi_components_neutral`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 243theorem rs_pattern_phi_components_neutral :
 244    rs_pattern ⟨0, by omega⟩ + rs_pattern ⟨2, by omega⟩ +
 245    rs_pattern ⟨4, by omega⟩ + rs_pattern ⟨6, by omega⟩ = 0 := by

proof body

Term-mode proof.

 246  simp only [rs_pattern]
 247  ring
 248
 249/-- The √2/2-indexed entries (k = 1, 3, 5, 7) independently sum to zero. -/

depends on (1)

Lean names referenced from this declaration's body.

rs_pattern in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use