mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Co-authored-by: Bhavik Mehta, Linus Sommer --- [](https://gitpod.io/from-referrer/)
- rename [Homeomorph.ofEmbedding](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Homeomorph.html#Homeomorph.ofEmbedding) to `Embedding.toHomeomorph` - move [Embedding.toHomeomeomorph_of_surjective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/IsLocalHomeomorph.html#Embedding.toHomeomeomorph_of_surjective) earlier (and remove the extra "meo") - rename [Homeomorph.homeomorphOfContinuousOpen](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Homeomorph.html#Homeomorph.homeomorphOfContinuousOpen) to `Homeomorph.ofContinuousOpenEquiv`. --- [](https://gitpod.io/from-referrer/)
Completes the proof of the group law in Jacobian coordinates, analogously to #8485 --- - [x] depends on: #9432 - [ ] depends on: #9433 - [ ] depends on:...
Define a addition-preserving bijection `toAffine_addEquiv` with the affine case to prove `Point` is an abelian group. This is the fourth in a series of four PRs leading to #9405 and...
Add a lemma showing that composing the comparison maps with a continuous function to a T3 space satisfying some conditions yield the same function. Co-authored with : María Inés de...
Define the analogous secant-and-tangent negation `neg` and addition `add` on `PointRep` over `F`, and lift them to `PointClass`. Define `Point` as a `PointClass` that is nonsingular. Prove in `neg_equiv` and...
Define auxiliary polynomials for the secant-and-tangent negation `neg` and addition `add` on `Fin 3 -> F`. Note that the group operations are defined from scratch instead of pulling back the...
--- [](https://gitpod.io/from-referrer/)
--- - [x] depends on: #13017 [](https://gitpod.io/from-referrer/)
A linter that makes sure that, when multiple goals are present, they are enclosed in `·`s. Adaptations (the order is chronological, there should be no dependency among them): * #12338,...
