theorem proved term proof

`plus_minus_indist`

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

formal statement (Lean)

 117theorem plus_minus_indist : Indistinguishable magnitudeRecognizer 3 (-3) := by

Term-mode proof.

 118  simp [Indistinguishable, magnitudeRecognizer]
 119
 120/-- **Theorem**: 2 ≁ 3 (different magnitudes) -/

From the project-wide theorem graph. These declarations reference this one in their body.

Lean names referenced from this declaration's body.

magnitudeRecognizer in IndisputableMonolith.RecogGeom.Examples decl_use
Indistinguishable in IndisputableMonolith.RecogGeom.Indistinguishable decl_use