Research proof index

left multiplication and right multiplication by a unit have the same Haar character on B ⊗ 𝔸_K^f. See also NumberField.FiniteAdeleRing.tensor_isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul which proves it for 𝔸_K^f ⊗ B.

left multiplication and right multiplication by a unit have the same Haar character on 𝔸_K^f ⊗ B. See also NumberField.FiniteAdeleRing.isCentralSimple_addHaarScalarFactor_left_mul_eq_right_mul which proves it for B ⊗ 𝔸_K^f.

The quotient of a Hausdorff second countable unimodular group by a central normal closed subgroup is still unimodular.

The analytic form of the main theorem (Silverman, Advanced topics, Theorem V.1.1(a)): for 0 < ‖q‖ < ‖u‖ < 1, Yₐ² + XₐYₐ = Xₐ³ - 5s₃(q)Xₐ - (5s₃(q) + 7s₅(q))/12. Proof sketch: the hypotheses ensure u ∉ qᶻ, and we may choose z, τ with e z = u, e τ = q, 0 < im z < im τ (so z ∉ Λ_τ). Substitute the four q-expansions into the differential...

The q-expansion of ℘' (Silverman, Advanced topics, Theorem I.6.2): under the hypotheses of weierstrassP_q_expansion, ℘'(z; Λ_τ) = (2πi)³ (Xₐ(e z, e τ) + 2Yₐ(e z, e τ)). Proof: as for weierstrassP_q_expansion, but simpler: group the absolutely convergent sum ℘'(z) = -2∑_ω (z - ω)⁻³ into rows ω = nτ + m (no regularising terms are needed here...

The descent lemma: a formal power series F ∈ ℚ(u)⟦q⟧ vanishes provided that, for infinitely many u₀ : ℂ, the evaluated series ∑ₙ Fₙ(u₀)q₀ⁿ converges with sum 0 for all sufficiently small nonzero q₀. Proof sketch: fix u₀. The function q₀ ↦ ∑ₙ Fₙ(u₀)q₀ⁿ is analytic on ‖q₀‖ < r (a power series converging pointwise on a disc is analytic there)...