chore: adaptations for nightly-2026-04-27#213

Merged

kim-em merged 164 commits into

bump/v4.31.0from

bump/nightly-2026-04-27

May 4, 2026

Commits on Mar 24, 2026

Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13086
leanprover-community-mathlib4-bot
committed
feat: add `Lean.Grind.PowIdentity` instance for finite fields

kim-em
and
claude
committed

Commits on Mar 26, 2026

Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13132
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13132
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13132
leanprover-community-mathlib4-bot
committed

Commits on Apr 1, 2026

Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13223
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13229
leanprover-community-mathlib4-bot
committed
chore: indent tactic blocks after `by` and `decreasing_by`

nomeata
and
claude
committed
chore: indent tactic block in EmptyLine test

nomeata
and
claude
committed
chore: indent expression continuations at column 0

nomeata
and
claude
committed
chore: indent expression continuations at column 0

nomeata
and
claude
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13229
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13223
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13229
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13229
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13223
leanprover-community-mathlib4-bot
committed

Commits on Apr 2, 2026

Update lean-toolchain for https://github.com/leanprover/lean4/pull/13229
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13223
leanprover-community-mathlib4-bot
committed
chore: fix linter tests
wkrozowski
committed

Commits on Apr 7, 2026

Commits on Apr 8, 2026

Commits on Apr 9, 2026

Commits on Apr 10, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
lake update
kim-em
committed
fixes
kim-em
committed
fix tests
kim-em
committed
ci: skip inputRev validation on nightly-testing branch

kim-em
and
claude
committed
chore: bump to nightly-2026-04-10
mathlib-nightly-testing[bot]
committed
merge lean-pr-testing-13262
mathlib-nightly-testing[bot]
committed
fix
Kha
committed
chore(nolints): add docBlame exceptions for auto-generated `instInhabited.default`

kim-em
and
claude
committed
fix(lint-style): filter out duplicate `Init` from `Mathlib.lean` imports

kim-em
and
claude
committed
fix
Kha
committed
fix plausible
Kha
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13346
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13346
leanprover-community-mathlib4-bot
committed

Commits on Apr 12, 2026

Commits on Apr 13, 2026

Merge master into nightly-testing
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13132
leanprover-community-mathlib4-bot
committed
chore: bump to nightly-2026-04-13
mathlib-nightly-testing[bot]
committed
Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/13325
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13325
leanprover-community-mathlib4-bot
committed
chore: silence simp `varHead` and `varOther` warnings
wkrozowski
committed
chore: silence `varHead` warning
wkrozowski
committed
chore: fix `globalAtrtributeIn` test
wkrozowski
committed
chore: fix `Archive` build
wkrozowski
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13325
leanprover-community-mathlib4-bot
committed
Update lean-toolchain for https://github.com/leanprover/lean4/pull/13325
leanprover-community-mathlib4-bot
committed
fix from nightly-testing
kim-em
committed

Commits on Apr 16, 2026

Commits on Apr 17, 2026

Commits on Apr 18, 2026

Commits on Apr 19, 2026

Commits on Apr 20, 2026

Commits on Apr 21, 2026

Commits on Apr 22, 2026

Commits on Apr 24, 2026

Commits on Apr 25, 2026

Commits on Apr 26, 2026

Commits on Apr 27, 2026

Commits on Apr 28, 2026