Junyan Xu

Thanks! However, I was distracted by other projects and didn't finish the proposed change to the prerequisite PR #7173, so I'm not sure that fixing build errors at this time...

I'd like to merge master into this soon, because I'm building on top of this branch but `WeierstrassCurve.map` is not available here. I expect this PR to be merged as...

Thanks!

[Here](https://github.com/leanprover-community/mathlib4/compare/EllipticCurve.Jacobian...EllipticCurve.Jacobian+?expand=1) are some additions and changes I made to the Jacobian file for the purpose of division polynomials, and maybe you want to incorporate them into one or more of...

Those addXYZ_self lemmas were mainly introduced to prove [addXYZ_smulField](https://github.com/leanprover-community/mathlib4/blob/DivisionPolynomial_smul/Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial.lean#L565-L567) for all m,n (by the way the branch is now sorry free). It's equally valid in the m=n case, and although...

Thanks and congratulations 🎉 maintainer merge

Seems we need to add Jacobian.lean to style-exceptions (see [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ERR_NUM_LIN/near/419415005)), or compress it (e.g. lemmas that fit in a single line, and blanks between such lemmas), or split it up.

Thanks 🎉 maintainer merge

Is it difficult to support? I just got a Windows laptop with 4060 (8GB VRAM) GPU last night, and have successfully run 4bit-quantized Mistral 7B via https://github.com/oobabooga/text-generation-webui#one-click-installers and also via...

Sorry, wrong PR. ~~I merged master in [this branch](https://github.com/leanprover-community/mathlib4/compare/EDSRec_merge?expand=1); please merge if it looks good.~~