Multiplication is commutative on the naturals
Closed
Theorem & proof
·
nat_mul_comm.lean
·
✓ verified
1
2
3
import Mathlib theorem nat_mul_comm (m n : Nat) : m * n = n * m :=Nat.mul_comm m n
Rewards pledged
No rewards pledged yet.