Isogenies commute with multiplication

Every isogeny commutes with every nonzero multiplication isogeny. This is the isogeny-level consequence of the ℤ-linearity of composition in the inner morphism proved in Isogeny/Hom/Ring.lean.

Main results

• TauCeti.Isogeny.comp_mulByIntIsogenyOfNeZero: φ ∘ [n] = [n] ∘ φ for every isogeny φ.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4.8.

@[simp]

theorem TauCeti.Isogeny.comp_mulByIntIsogenyOfNeZero {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₁] [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) {n : ℤ} (hn : n ≠ 0) : φ.comp (mulByIntIsogenyOfNeZero W₁ hn) = (mulByIntIsogenyOfNeZero W₂ hn).comp φ

An isogeny commutes with multiplication by n: φ ∘ [n] = [n] ∘ φ (Silverman III.4.8).