mathlib

79f700b0 - feat(linear_algebra/affine_space/affine_map): `line_map_eq_` `iff` lemmas (#17658)

feat(linear_algebra/affine_space/affine_map): `line_map_eq_` `iff` lemmas (#17658) Add lemmas giving `iff` conditions (given `no_zero_smul_divisors`) for `line_map` to produce the left or right point, or for `line_map` with two scalars to be equal.