Def Nonneg.coeAddMonoidHom

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.coeAddMonoidHom View on Github →

2023-02-11 09:23

Mathlib/Algebra/Order/Nonneg/Ring.lean

feat: port Algebra.Order.Nonneg.Ring (#1260) …

Added Nonneg.coeAddMonoidHom View on Github →