Zulip Chat Archive
Stream: PR reviews
Topic: 2816 affine spaces
Yury G. Kudryashov (May 31 2020 at 02:22):
I made a suggestion to change design of affine subspaces. I'm not sure which way is better, and it would be nice to get more opinions.
https://github.com/leanprover-community/mathlib/pull/2816/files#r432903174
Last updated: Dec 20 2023 at 11:08 UTC