Commit 2024-10-07 17:59 4c163af3
View on Github →chore(Mathlib/Data/Nat/Defs): remove Nat.add_def (#17488)
... since this is a duplicate of Nat.add_eq.
Drive-by: clean up a proof where add_def was used a bit.
chore(Mathlib/Data/Nat/Defs): remove Nat.add_def (#17488)
... since this is a duplicate of Nat.add_eq.
Drive-by: clean up a proof where add_def was used a bit.