mathlib
ee768c0f - fix(linear_algebra/affine_space/affine_subspace): remove obsolete comment (#17586)

Commit
3 years ago
fix(linear_algebra/affine_space/affine_subspace): remove obsolete comment (#17586) This comment is no longer needed after notations for norms and "parallel" were fixed.
Author
Parents
Loading