[Merged by Bors] - feat(NumberTheory/EllipticDivisibilitySequence): expose the auxiliary sequence

[Multramate]

Expose the auxiliary sequences associated to normalised elliptic divisibility sequences along with their corresponding API, and fix the comments under implementation notes. This is needed to define $n$-division polynomials of elliptic curves in a later downstream file as univariate polynomials with the factor of the bivariate $2$-division polynomial omitted.

---

[MichaelStollBayreuth]

Suggested change

	preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * (if Even m then 1 else b)
	preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) ^ 3 * (if Even m then 1 else b)

From the Style Guide: "This rule, i.e., indent an additional two spaces, applies more generally whenever a term spans multiple lines."

[alreadydone]

@Multramate Can you merge master and fix the indentation as pointed out by @MichaelStollBayreuth? I'd like to use preNormEDS to define $\psi^c_n=\psi_{2n}/\psi_n=(\psi_{n-1}^2\psi_{n+2}-\psi_{n-2}\psi_{n+1}^2)/\psi_2$ in my notes in a division-free way. I think the correct definition is normEDSCompl n := (preNormEDS (n-1) * preNormEDS (n+2) ^ 2 - preNormEDS (n-2) * preNormEDS (n+1) ^ 2) * (if Even n then 1 else b) where preNormEDS is applied to the parameters b^4, c, d, and I'll then show normEDS n * normEDSCompl n = normEDS (2 * n).

[alreadydone]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alreadydone.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style