Zulip Chat Archive
Stream: nightly-testing
Topic: nightly#31 adaptations for nightly-2025-08-10
github mathlib4 bot (Aug 11 2025 at 05:29):
chore: adaptations for nightly-2025-08-10 nightly#31 Please review this PR. At the next toolchain release this diff will land in 'master'.
Kim Morrison (Aug 11 2025 at 06:12):
Looks good to me besides one regression noted as an #adaptation_note in Mathlib/RingTheory/Ideal/Operations.lean which I'm still diagnosing.
Last updated: Dec 20 2025 at 21:32 UTC