274theorem toNat_mul (a b : LogicNat) : 275 toNat (a * b) = toNat a * toNat b := by
proof body
Term-mode proof.
276 induction b with 277 | identity => 278 show toNat (a * zero) = toNat a * toNat zero 279 rw [mul_zero, toNat_zero, Nat.mul_zero] 280 | step b ih => 281 show toNat (a * succ b) = toNat a * toNat (succ b) 282 rw [mul_succ, toNat_succ, toNat_add, ih, Nat.mul_succ] 283 284/-- Left cancellation: `a + b = a + c ⇒ b = c`. Proved by transferring 285to `Nat` via the recovery isomorphism. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.