[Merged by Bors] - feat(data/equiv/mul_add): use @[simps]
#7213
Conversation
github-actions
bot
added
the
merge-conflict
|
Thank you for taking care of this! |
fpvandoorn
force-pushed
the
mul_add_simps
branch
from
f0a8906
to
7ac0a05
Compare
fpvandoorn
added
awaiting-review
github-actions
bot
removed
the
merge-conflict
| @@ -389,7 +389,7 @@ def comp_hom : (normed_group_hom V₂ V₃) →+ (normed_group_hom V₁ V₂) | |||
| add_monoid_hom.mk' (λ g, add_monoid_hom.mk' (λ f, g.comp f) | |||
| (by { intros, ext, exact g.map_add _ _ })) | |||
| (by { intros, ext, simp only [comp_apply, pi.add_apply, function.comp_app, | |||
| add_monoid_hom.add_apply, add_monoid_hom.coe_mk', coe_add] }) | |||
| add_monoid_hom.add_apply, add_monoid_hom.mk'_apply, coe_add] }) | |||
There was a problem hiding this comment.
What is the new statement of mk'_apply?
There was a problem hiding this comment.
It is the same as the current add_monoid_hom.coe_mk', i.e. an equality between functions. I tried to keep the generated lemmas as close to the existing ones, except for the name.
It is currently not possible in the @[simps] framework to sometimes use a projection with one name _apply and sometimes with a different name _coe (though this would be easy to add).
There was a problem hiding this comment.
_apply feels like the wrong name here - I'm not sure we should be using simps to save lines if it comes at the expense of generating an unusual name.
|
bors merge |
github-actions
bot
added
ready-to-merge
| @[simp] lemma coe_mul_left' (a : G) (ha : a ≠ 0) : ⇑(equiv.mul_left' a ha) = (*) a := rfl | ||
|
|
||
| @[simp] lemma mul_left'_symm_apply (a : G) (ha : a ≠ 0) : | ||
| ((equiv.mul_left' a ha).symm : G → G) = (*) a⁻¹ := rfl |
There was a problem hiding this comment.
Do the generated lemmas use λ x, a * x or (*) a? The latter seems more desirable, but I don't know about about simps to know if its what actually happens.
|
Build failed (retrying...): |
|
Build failed (retrying...): |
|
Failure was due to |
|
Already running a review |
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
@[simps]@[simps]
Add some
@[simps]for some algebra maps. This came up in #6795.WIP until this builds.