Zulip Chat Archive
Stream: Is there code for X?
Topic: Infinite sum of groups
Violeta Hernández (Jan 05 2026 at 06:20):
What's the Lean way to write down a direct sum of a family ∀ i, Group (G i) of groups? Is it with DFinsupp, or something else?
Yury G. Kudryashov (Jan 05 2026 at 06:28):
See also docs#DirectSum
Last updated: Feb 28 2026 at 14:05 UTC