commit: f2e191d0afbb5adcc6f12e1779c8b141fc9af996

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

Sun Nov 23 19:11:13 2025 -0800
committer: GitHub <noreply@github.com>

Mon Nov 24 03:11:13 2025 +0000
tree: a8f7a3b5bdaa2b525aa7b03ba6e2bdfdb122eed0
parent: 0b173923f424f4c45392e0c5aa812ba11578d011 [diff]

refactor: `grind linarith` ring normalization (#11334)

This PR adds an explicit normalization layer for ring constraints in the
`grind linarith` module. For example, it will be used to clean up
denominators when the ring is a field.

7 files changed

tree: a8f7a3b5bdaa2b525aa7b03ba6e2bdfdb122eed0

README.md

This is the repository for Lean 4.

About

Installation

See Install Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.