pith. machine review for the scientific record. sign in
theorem proved term proof

RCLCombiner_zero_separatelyAdditive

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 130theorem RCLCombiner_zero_separatelyAdditive :
 131    SeparatelyAdditive (RCLCombiner 0) := by

proof body

Term-mode proof.

 132  refine ⟨fun u => 2 * u, fun v => 2 * v, ?_⟩
 133  intro u v
 134  unfold RCLCombiner
 135  ring
 136
 137/-- For `c ≠ 0`, the RCL combiner has nonvanishing interaction defect
 138at the test point `(1, 1)`. -/

depends on (5)

Lean names referenced from this declaration's body.