Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-01-25 11:06 e7e2ba8a

View on Github →

feat(algebra/order/ring/with_top): ring covariance & ordered ring typeclasses for with_bot (#18149) mathlib4 PR: https://github.com/leanprover-community/mathlib4/pull/1508

Estimated changes

Modified src/algebra/order/monoid/with_top.lean

added theorem with_bot.coe_le_one

added theorem with_bot.one_le_coe

added theorem with_top.coe_le_one

added theorem with_top.one_le_coe

Modified src/algebra/order/ring/with_top.lean

Modified src/data/nat/with_bot.lean

modified theorem nat.with_bot.coe_nonneg