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

D_quad1_not_axisAdditive

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)

 208theorem D_quad1_not_axisAdditive : ¬ AxisAdditive correction_D_quad1 := by

proof body

Term-mode proof.

 209  intro h
 210  rcases h with ⟨h0, hadd⟩
 211  have h11 : correction_D_quad1 (1 + 1) = correction_D_quad1 1 + correction_D_quad1 1 := hadd 1 1
 212  unfold correction_D_quad1 at h11
 213  norm_num at h11
 214
 215/-- D²/6 is not axis-additive (witness: 1+1). -/

depends on (6)

Lean names referenced from this declaration's body.