commit: 305fba625d46a676c549c3129dc98d638d281781

[log]
author: Kim Morrison <scott.morrison@gmail.com>

Thu May 15 14:17:46 2025 +0800
committer: GitHub <noreply@github.com>

Thu May 15 06:17:46 2025 +0000
tree: cd6e462f1036721ac0536cd38b75529e1002a7be
parent: 83001213e3095768dcf6e6a24c81b782db5ea583 [diff]

feat: missing lemmas about Int order/multiplication (#8346)

This PR adds some missing lemmas about consequences of
positivity/non-negativity of `a * b : Int`.

src/Init/Data/Int/Order.lean[diff]

1 file changed

tree: cd6e462f1036721ac0536cd38b75529e1002a7be

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.