ℒ̃ is stable under complex conjugation

Proved

DiazModulus.logAlgTilde_conj_stable

by carlok · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theorytranscendence

Here $\mathcal{L}$ is the set of logarithms of algebraic numbers, and $\widetilde{\mathcal{L}}$ is the $\overline{\mathbb{Q}}$ -vector space spanned by $1$ and $\mathcal{L}$ .

If $z \in \widetilde{\mathcal{L}}$ , then $\bar z \in \widetilde{\mathcal{L}}$ .

Proof. By induction on the span: $\bar 1 = 1$ ; the conjugate of a logarithm of an algebraic number is a logarithm of the conjugate number (DiazModulus.logAlg_conj_stable); and the conjugate of an algebraic coefficient is algebraic.

Novelty. None: a standard fact, used throughout Diaz (2004, 2007).

Preamble

import Definitions.Def_DiazModulus

Formal statement

open Complex ComplexConjugate

namespace DiazModulus

/-- `ℒ̃` is stable under complex conjugation. -/
theorem logAlgTilde_conj_stable (z : ℂ) (h : z ∈ LogAlgTilde) : conj z ∈ LogAlgTilde := by
  sorry

end DiazModulus

Source

Standard; used throughout G. Diaz, Utilisation de la conjugaison complexe dans l'étude de la transcendance de valeurs de la fonction exponentielle usuelle, J. Théor. Nombres Bordeaux 16 (2004), 535–553 and G. Diaz, Produits et quotients de combinaisons linéaires de logarithmes de nombres algébriques : conjectures et résultats partiels, J. Théor. Nombres Bordeaux 19 (2007), 373–391. Formal proof: Diaz modulus mission, 1 October 2026 (C. Perassi).

View graph