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

toRat_neg

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)

  92theorem toRat_neg (v : MultIndex) : toRat (-v) = (toRat v)⁻¹ := by

proof body

Tactic-mode proof.

  93  have h_sum : toRat ((-v) + v) = toRat (-v) * toRat v := toRat_add (-v) v
  94  have h_zero : ((-v) + v) = (0 : MultIndex) := by simp
  95  rw [h_zero, toRat_zero] at h_sum
  96  have hv_pos : 0 < toRat v := toRat_pos v
  97  have hv_ne : toRat v ≠ 0 := ne_of_gt hv_pos
  98  field_simp [hv_ne]
  99  linarith [h_sum]
 100
 101/-- Reciprocal symmetry of `J` at the index level: `J(1/q) = J(q)`. -/

used by (3)

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

depends on (14)

Lean names referenced from this declaration's body.