Commit 2026-03-26 13:05 26d13c64
View on Github →chore(Mathlib/Algebra/Algebra/Pi.lean): automated extraction (#37201) This PR was automatically created from PR #34727 by @ocfnash via a review comment by @jcommelin.
chore(Mathlib/Algebra/Algebra/Pi.lean): automated extraction (#37201) This PR was automatically created from PR #34727 by @ocfnash via a review comment by @jcommelin.