[Merged by Bors] - feat: Function.End.one_def and mul_def#6802
[Merged by Bors] - feat: Function.End.one_def and mul_def#6802ChrisHughes24 wants to merge 2 commits intomasterfrom
Conversation
ChrisHughes24
commented
Aug 26, 2023
| rfl | ||
| #align function.End.smul_def Function.End.smul_def | ||
|
|
||
| theorem Function.End.mul_def (f g : Function.End α) : (f * g) = f ∘ g := |
There was a problem hiding this comment.
This feels like defeq abuse to me; I'd be happier with something like
| theorem Function.End.mul_def (f g : Function.End α) : (f * g) = f ∘ g := | |
| theorem Function.End.mul_def (f g : Function.End α) : (toEnd f * toEnd g) = toEnd (f ∘ g) := |
There was a problem hiding this comment.
I'd be happy with a TODO comment instead, as long as these aren't simp lemmas
There was a problem hiding this comment.
I'm not sure exactly what is TODO. There are a few ways toEnd could be done, we could completely forbid using End as a function without using a FunLike instance, or be less strict.
There was a problem hiding this comment.
I added some comments
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |