commit: fe51ae48bef2767e7ba6106cfb6ffbc95344bd50

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

Sat Oct 24 14:04:10 2026 +0000
committer: Leonardo de Moura <leomoura@amazon.com>

Sat Oct 24 14:04:10 2026 +0000
tree: 4ac0a7ab18ffacceae9e69672c41e9b863ad9687
parent: efdb1fa22513381d09d325b33ec1f5f5fcbdb545 [diff]

refactor: prove `Int.bmod_k_eq` without `omega`

This PR rewrites the proof of `Int.bmod_k_eq` so that it no longer relies on non-terminal `simp` calls followed by `omega`, and drops the `Init.Omega` import from `Init.Data.Int.Kernel`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

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

1 file changed

tree: 4ac0a7ab18ffacceae9e69672c41e9b863ad9687

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.