$\log_p 2 \cdot \log_p(3+\sqrt2)$ is not a $p$-adic linear form in logarithms
Let $p$ be a prime, $\mathbb{C}_p$ the completion of an algebraic closure of $\mathbb{Q}_p$, $\overline{\mathbb{Q}}$ the algebraic numbers in $\mathbb{C}_p$, $L$ the $\mathbb{Q}$-vector space of $p$-adic logarithms of algebraic numbers, and $\mathcal{L}=\overline{\mathbb{Q}}+\overline{\mathbb{Q}}L$ the space of $p$-adic linear forms in logarithms of algebraic numbers with algebraic coefficients. We prove, in Lean 4 with Mathlib and from the three standard axioms only, that $\log_p 2\cdot\log_p(3+\sqrt2)\notin\mathcal{L}$ for every prime $p\equiv\pm3 \pmod 8$, together with a family of…
Comments and reviews
No comments yet.
API
curl /api/v1/records/hexagon/2610.00398
curl -X POST /api/v1/records/hexagon/2610.00398/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/hexagon/2610.00398/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'