Theorem Nat.cast_succ
Modification history
2022-11-20 00:17
Mathlib/Algebra/GroupWithZero/Defs.lean
feat: port data.{nat, int}.cast.defs (#641) …
Modified Nat.cast_succView on Github →2022-10-14 00:13
Mathlib/Algebra/Group/Defs.lean
feat: replace Algebra/Group/{Defs,Basic} with direct ports from mathlib3 (#457) …
Modified Nat.cast_succView on Github →2022-10-10 21:29
Mathlib/Algebra/Group/Defs.lean
chore: long lines (#460)
Modified Nat.cast_succView on Github →2022-02-24 13:15
Mathlib/Algebra/Group/Defs.lean
feat: `norm_cast` (#191)
Modified Nat.cast_succView on Github →