commit: 197f9f1ef73f4ddde03f4b58c08b19c0fa809ab7

[log]
author: Kim Morrison <kim@tqft.net>

Fri Sep 11 04:41:38 2026 +0000
committer: Kim Morrison <kim@tqft.net>

Fri Sep 11 04:41:38 2026 +0000
tree: 3fed2e85867655aa4846c2ff2d3d1b844683ef2d
parent: f1ec82e73a29080c50aff64703259c7eff7f36a1 [diff]

fix: keep `@[grind inj]` theorems in `grobner [...]`

Use the default `@[grind]` extension state with only its E-matching rules cleared, rather than the `only` state, so injectivity theorems remain available when a parameter list is given.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>

3 files changed

tree: 3fed2e85867655aa4846c2ff2d3d1b844683ef2d

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.