Def Nonneg.coeRingHom

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

2023-02-11 09:23

Mathlib/Algebra/Order/Nonneg/Ring.lean

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

Added Nonneg.coeRingHom View on Github →