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