commit: 017168a9ae73188c275086af2771f7acebe05ec0

[log]
author: Leonardo de Moura <leomoura@amazon.com>

Sat Jun 14 21:54:16 2025 -0700
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Jun 14 21:56:12 2025 -0700
tree: 7eff243aba0080aa15c041dd3a92b5e19b3515c6
parent: f86560d1343a5c71af7579ac6bf004f7315c9eaf [diff]

feat: add instance `IsCharP R 0` for a linear ordered field `R`

This PR adds the following instance
```
instance [Field α] [LinearOrder α] [Ring.IsOrdered α] : IsCharP α 0
```
The goal is to ensure we do not perform unnecessary case-splits in our
test suite.

2 files changed

tree: 7eff243aba0080aa15c041dd3a92b5e19b3515c6

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.