Commit 2020-06-01 19:40 085aadeb

View on Github →

chore(linear_algebra/affine_space): use implicit args (#2905) Whenever we have an argument f : affine_map k V P, Lean can figure out k, V, and P.

Estimated changes

Modified src/linear_algebra/affine_space.lean

added theorem affine_map.coe_comp

added theorem affine_map.coe_id

modified theorem affine_map.comp_apply

modified theorem affine_map.id_apply