Theorem Nat.cast_succ_succ

Modification history

2022-02-23 09:06

Mathlib/Algebra/Ring/Basic.lean

feat: `AddMonoidWithOne`, `AddGroupWithOne` (#206) …

Deleted Nat.cast_succ_succ View on Github →

2022-02-01 18:42

Mathlib/Algebra/Ring/Basic.lean

refactor: remove numeric (#177) …

Added Nat.cast_succ_succ View on Github →