Theorems · Definition · number theory

IsEllipticNet.atomRel

{R : Type u_1} → [CommRing R] → (ℤ → R) → ℤ → ℤ → ℤ → ℤ → R

The elliptic relator ERₐ(a, b, c, d) obtained by a change of variables in ER(p, q, r, s) (see IsEllipticNet.rel_eq and IsEllipticNet.atomRel_eq). Note that this is defined in terms of elliptic atoms, and hence should only be used when a, b, c, and d have the same parity.

Defined in

Mathlib.NumberTheory.EllipticDivisibilitySequence

Cited by

20 results in Mathlib

Foundations

Depth 22 from the axioms · uses no axioms

Assumes

CommRing