Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-31 08:43 1f616214

View on Github →

feat(linear_algebra/affine_space/affine_map): add affine_map.proj (#4850)

Estimated changes

Modified src/linear_algebra/affine_space/affine_map.lean

added theorem affine_map.pi_line_map_apply

added def affine_map.proj

added theorem affine_map.proj_apply

added theorem affine_map.proj_linear

Modified src/linear_algebra/affine_space/midpoint.lean

added theorem pi_midpoint_apply