Def Nat.cast

Modification history

2022-11-20 00:17

Mathlib/Algebra/GroupWithZero/Defs.lean

feat: port data.{nat, int}.cast.defs (#641) …

Deleted Nat.cast View 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 View on Github →

2022-02-23 09:06

Mathlib/Algebra/Group/Defs.lean

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

Added Nat.cast View on Github →