Complex conjugation does not commute with multiplication by
ProvedDiaz.conj_not_linear_of_Idiaz-modulus-leannumber-theory
For the imaginary unit ,
Why. Conjugation is conjugate-linear, not linear: , and . Taking already refutes the displayed identity.
Role. This is the concrete instance of the previous remark: conjugation is not linear over any base field containing — in particular not over , 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 -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 sorrySource