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: May 02 2025 at 03:31 UTC