Theorem Nonneg.mk_natCast

Modification history

2024-07-15 23:26

Mathlib/Algebra/Order/Nonneg/Ring.lean

chore (Algebra.Order.Nonneg.Ring): split into unbundled and bundled ordered ring files (#14370) …

Modified Nonneg.mk_natCast View on Github →

2024-04-17 11:15

Mathlib/Algebra/Order/Nonneg/Ring.lean

chore: Rename `nat_cast`/`int_cast`/`rat_cast` to `natCast`/`intCast`/`ratCast` (#11486) …

Added Nonneg.mk_natCast View on Github →