Commit 2023-01-07 19:13 d5a3ae40

feat: port Algebra.Module.Pi (#1283) One earlier failure was extensively discussed:

• https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Performance.20issue.20with.20.60CompleteBooleanAlgebra.60/near/319019205
• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20class.20inference.20looping and is fixed as of https://github.com/leanprover/lean4/commit/70a6c06eef060d8e14869e2848749287e5364742, in mathlib as of the bump #1335. Another failure posted to Zulip and the Lean 4 repo
• https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/type.20class.20inference.20failure.20in.20pi.20type
• https://github.com/leanprover/lean4/issues/2011 and is fixed as of https://github.com/leanprover/lean4/commit/fedf235cba35ed8bf6bf571cf38e6d8536b904ac, in mathlib as of the bump #1397. There is one more mysterious apply failure, now worked around; we should track this down someday.
• depends on: #1397