[Merged by Bors] - chore: adaptations for nightly-2026-04-19#210

Closed

kim-em wants to merge 126 commits into

bump/v4.31.0from

bump/nightly-2026-04-19

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 15, 2026

Commits on Apr 16, 2026

Commits on Apr 17, 2026

Commits on Apr 18, 2026

Commits on Apr 19, 2026