Theorem Num.ofNat'_one

Modification history

2025-12-06 18:41

Mathlib/Data/Num/Lemmas.lean

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

Modified Num.ofNat'_one View on Github →

2023-04-10 15:18

Mathlib/Data/Num/Lemmas.lean

feat: port Data.Num.Lemmas (#2784)

Added Num.ofNat'_one View on Github →