Commit 2023-01-25 14:27 98bc5f26

View on Github →

feat: ring covariance & ordered ring typeclasses for WithBot (#1508) mathlib3 PR: https://github.com/leanprover-community/mathlib/pull/18149

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

added theorem WithBot.coe_le_one

added theorem WithBot.one_le_coe

added theorem WithTop.coe_le_one

added theorem WithTop.one_le_coe

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

Modified Mathlib/Data/Nat/WithBot.lean