Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Complex conjugation does not commute with multiplication by iii

Proved
Diaz.conj_not_linear_of_I

by carlok · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theory

For the imaginary unit i∈Ci \in \mathbb{C}i∈C,

¬ (∀ z∈C,iz‾=i zˉ).\neg\ \Big(\forall\, z \in \mathbb{C}, \quad \overline{i z} = i\,\bar z\Big).¬ (∀z∈C,iz=izˉ).

Why. Conjugation is conjugate-linear, not linear: iz‾=iˉ zˉ=−i zˉ\overline{iz} = \bar i\,\bar z = -i\,\bar ziz=iˉzˉ=−izˉ, and −i≠i-i \neq i−i=i. Taking z=1z = 1z=1 already refutes the displayed identity.

Role. This is the concrete instance of the previous remark: conjugation is not linear over any base field containing iii — in particular not over Qˉ\bar{\mathbb{Q}}Qˉ​, the base that Diaz's modulus conjecture is about. It is recorded because an earlier draft of the accompanying note asserted the opposite in the guise of calling the involution on the hull a Qˉ\bar{\mathbb{Q}}Qˉ​-algebra involution.

Preamble
import Mathlib

open ComplexConjugate
variable (K : Subfield ℂ) (u : ℂ)
variable {K u}
Formal statement
theorem Diaz.conj_not_linear_of_I :
    ¬ (∀ z : ℂ, conj (Complex.I * z) = Complex.I * conj z) := by sorry
Source
https://github.com/carlok/diaz-modulus-lean/blob/801802b8ac052dff50baf17ac4a7ceac3e994ca9/Diaz/Closure.lean#L115-L121

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactJoin Slack© 2026 Prove2Me