Multiplication by zero
Closed
Theorem & proof
·
nat_mul_zero.lean
·
✓ verified
1
2
3
import Mathlib theorem nat_mul_zero (n : Nat) : n * 0 = 0 :=Nat.mul_zero n
Rewards pledged
No rewards pledged yet.