Commit 2026-02-26 09:42 835018ca
View on Github →chore(Mathlib/RingTheory/Algebraic/Basic.lean): automated extraction (#35801) This PR was automatically created from PR #34215 by @justus-springer via a review comment by @jcommelin.
chore(Mathlib/RingTheory/Algebraic/Basic.lean): automated extraction (#35801) This PR was automatically created from PR #34215 by @justus-springer via a review comment by @jcommelin.