[Merged by Bors] - chore(linear_algebra): fix/add coe_fn simp lemmas
#7015
Conversation
* move `@[simp]` from `linear_map.comp_apply` to new `linear_map.coe_comp`; * rename `linear_map.comp_coe` to `linear_map.coe_comp`, swap LHS&RHS; * add `linear_map.coe_proj`, move `@[simp]` from `linear_map.proj_apply`.
urkud
added
awaiting-review
|
|
||
| @[norm_cast] | ||
| lemma comp_coe : (f : M₂ → M₃) ∘ (g : M → M₂) = f.comp g := rfl | ||
| @[simp, norm_cast] lemma coe_comp : (f.comp g : M → M₃) = f ∘ g := rfl |
There was a problem hiding this comment.
| @[simp, norm_cast] lemma coe_comp : (f.comp g : M → M₃) = f ∘ g := rfl | |
| @[simp, norm_cast] lemma coe_comp : ⇑(f.comp g) = f ∘ g := rfl |
There was a problem hiding this comment.
Why is using the arrow preferred over an explicit type annotation?
There was a problem hiding this comment.
The main reasons are:
- It's shorter
- we do that elsewhere
- It matches what the goal view shows and what doc-gen shows
It doesn't actually make any difference to lean.
There was a problem hiding this comment.
I prefer the explicit type annotation basically because I might be browsing the code outside of an editor or even if I am in the editor, if I'm looking at this lemma I might be too lazy to click around to see what the coercion is.
(Ultimately I don't think this is a big deal, so Yury should just go with whichever he wants.)
There was a problem hiding this comment.
@eric-wieser "Arrows" version doesn't work with the current state of leanprover-community/lean#557 (I hope, it will be fixed), so I'll leave it as is.
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bryangingechen
added
delegated
|
bors merge |
github-actions
bot
added
the
ready-to-merge
* move `@[simp]` from `linear_map.comp_apply` to new `linear_map.coe_comp`; * rename `linear_map.comp_coe` to `linear_map.coe_comp`, swap LHS&RHS; * add `linear_map.coe_proj`, move `@[simp]` from `linear_map.proj_apply`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
coe_fn simp lemmascoe_fn simp lemmas
@[simp]fromlinear_map.comp_applyto newlinear_map.coe_comp;linear_map.comp_coetolinear_map.coe_comp, swap LHS&RHS;linear_map.coe_proj, move@[simp]fromlinear_map.proj_apply.