[Merged by Bors] - chore(linear_algebra/affine_space): use implicit args

[urkud]

Whenever we have an argument f : affine_map k V P, Lean can figure out k, V, and P.

[jsm28]

I think this is fine. Affine spaces and torsors do often need explicit type arguments (when a definition only has points as explicit arguments, it seems Lean can't figure out the types of vectors and scalars; when it only has points and vectors as explicit arguments, it seems Lean can't figure out the type of scalars, for example), but this case doesn't need those explicit arguments (and there may be other definitions that are also taking more explicit type arguments than necessary).

[urkud]

I'm making more args implicit. Should be ready soon.

[jcommelin]

@urkud I'm still trying to get a feel for the new superpowers that coercion to function now has. Should P1 even be implicit in .id itself? I guess that almost always it can be inferred from the context, and it looks a lot nicer (in my opinion) without the P1.

[urkud]

@jcommelin I think that this kind of a refactor should be done simultaneously for all bundled homs.

[jcommelin]

Ok, that's a fair point.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests and docs