New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(AlgebraicGeometry/EllipticCurve/*): rename baseChange to map #9744
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
bors d+
|
||
lemma equation_iff_baseChange {φ : R →+* A} (hφ : Function.Injective φ) (x y : R) : | ||
W.equation x y ↔ (W.baseChange φ).toAffine.equation (φ x) (φ y) := by | ||
lemma map_equation {φ : R →+* A} (hφ : Function.Injective φ) (x y : R) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Shouldn't the name still contain iff
? Also below.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Eh, I think this is probably fine.
✌️ Multramate can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…#9744) This is in accordance with other similar definitions e.g. `Polynomial.map`. It turns out that rewrite lemmas of the form `(W.map (φ.comp ψ)).negY/addX/addY = ψ ((W.map φ).negY/addX/addY)` are rather annoying to use, so they are replaced with the original `baseChange` functionality that says `(W.baseChange B).negY/addX/addY = ψ ((W.baseChange A).negY/addX/addY)`. This addresses the issue in #9596 pointed out by @riccardobrasca, but for the Weierstrass curve `W` rather than its points.
Build failed (retrying...): |
…#9744) This is in accordance with other similar definitions e.g. `Polynomial.map`. It turns out that rewrite lemmas of the form `(W.map (φ.comp ψ)).negY/addX/addY = ψ ((W.map φ).negY/addX/addY)` are rather annoying to use, so they are replaced with the original `baseChange` functionality that says `(W.baseChange B).negY/addX/addY = ψ ((W.baseChange A).negY/addX/addY)`. This addresses the issue in #9596 pointed out by @riccardobrasca, but for the Weierstrass curve `W` rather than its points.
Pull request successfully merged into master. Build succeeded: |
…#9744) This is in accordance with other similar definitions e.g. `Polynomial.map`. It turns out that rewrite lemmas of the form `(W.map (φ.comp ψ)).negY/addX/addY = ψ ((W.map φ).negY/addX/addY)` are rather annoying to use, so they are replaced with the original `baseChange` functionality that says `(W.baseChange B).negY/addX/addY = ψ ((W.baseChange A).negY/addX/addY)`. This addresses the issue in #9596 pointed out by @riccardobrasca, but for the Weierstrass curve `W` rather than its points.
…#9744) This is in accordance with other similar definitions e.g. `Polynomial.map`. It turns out that rewrite lemmas of the form `(W.map (φ.comp ψ)).negY/addX/addY = ψ ((W.map φ).negY/addX/addY)` are rather annoying to use, so they are replaced with the original `baseChange` functionality that says `(W.baseChange B).negY/addX/addY = ψ ((W.baseChange A).negY/addX/addY)`. This addresses the issue in #9596 pointed out by @riccardobrasca, but for the Weierstrass curve `W` rather than its points.
…#9744) This is in accordance with other similar definitions e.g. `Polynomial.map`. It turns out that rewrite lemmas of the form `(W.map (φ.comp ψ)).negY/addX/addY = ψ ((W.map φ).negY/addX/addY)` are rather annoying to use, so they are replaced with the original `baseChange` functionality that says `(W.baseChange B).negY/addX/addY = ψ ((W.baseChange A).negY/addX/addY)`. This addresses the issue in #9596 pointed out by @riccardobrasca, but for the Weierstrass curve `W` rather than its points.
…#9744) This is in accordance with other similar definitions e.g. `Polynomial.map`. It turns out that rewrite lemmas of the form `(W.map (φ.comp ψ)).negY/addX/addY = ψ ((W.map φ).negY/addX/addY)` are rather annoying to use, so they are replaced with the original `baseChange` functionality that says `(W.baseChange B).negY/addX/addY = ψ ((W.baseChange A).negY/addX/addY)`. This addresses the issue in #9596 pointed out by @riccardobrasca, but for the Weierstrass curve `W` rather than its points.
This is in accordance with other similar definitions e.g.
Polynomial.map
. It turns out that rewrite lemmas of the form(W.map (φ.comp ψ)).negY/addX/addY = ψ ((W.map φ).negY/addX/addY)
are rather annoying to use, so they are replaced with the originalbaseChange
functionality that says(W.baseChange B).negY/addX/addY = ψ ((W.baseChange A).negY/addX/addY)
. This addresses the issue in #9596 pointed out by @riccardobrasca, but for the Weierstrass curveW
rather than its points.