Commit 2025-12-06 18:41 30c71040

View on Github →

chore(Data/Num): remove use of erw in ofNat'_one (#32504)

Estimated changes

modified theorem Num.ofNat'_one