independent): allow dot notation on affine_independent (#8974)

Commit

4 years ago

chore(linear_algebra/affine_space/independent): allow dot notation on affine_independent (#8974) This renames a few lemmas to make dot notation on `affine_independent` possible.

Author

YaelDillies

Parents

7a2ccb6a

mathlib3 3d31c2dd - chore(linear_algebra/affine_space/independent): allow dot notation on affine_independent (#8974)

mathlib3
3d31c2dd - chore(linear_algebra/affine_space/independent): allow dot notation on affine_independent (#8974)