affine_equiv): extra lemmas and docstrings (#14319)

Commit

3 years ago

feat(linear_algebra/affine_space/affine_equiv): extra lemmas and docstrings (#14319) I was struggling to find this definition, so added some more lemmas and a docstring.

Author

eric-wieser

Parents

aa6dc575

mathlib 9288a2d9 - feat(linear_algebra/affine_space/affine_equiv): extra lemmas and docstrings (#14319)

mathlib
9288a2d9 - feat(linear_algebra/affine_space/affine_equiv): extra lemmas and docstrings (#14319)