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

sound

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)

  90theorem sound (a b c d : LogicInt) (hb : b ≠ 0) (hd : d ≠ 0)
  91    (h : a * d = c * b) : mk a b hb = mk c d hd := by

proof body

Term-mode proof.

  92  apply Quotient.sound
  93  show a * d = c * b
  94  exact h
  95
  96/-! ## 3. Embedding LogicInt into LogicRat -/
  97
  98/-- The natural injection `LogicInt ↪ LogicRat` sending `n` to `n/1`. -/

used by (21)

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

depends on (6)

Lean names referenced from this declaration's body.