Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-06 17:52 339c2c35

View on Github →

feat(linear_algebra/affine_space/independent): affine independence is preserved by affine maps (#9005)

Estimated changes

Modified src/linear_algebra/affine_space/affine_map.lean

added theorem affine_map.injective_iff_linear_injective

Modified src/linear_algebra/affine_space/independent.lean

added theorem affine_independent.map'

added theorem affine_independent.of_comp

added theorem affine_map.affine_independent_iff