Zulip Chat Archive
Stream: PR reviews
Topic: Boring linear algebra results: #25166, #25169, #25142
Eric Wieser (May 25 2025 at 12:16):
These three PRs (#25166, #25169, #25142) add a collection of boring results that are a step towards removing a Module.Finite assumption from Module.Free.multilinearMap. One of them raises a naming inconsistency.
Last updated: Dec 20 2025 at 21:32 UTC