Explicit quadratic conjugation formulas. These identify the two-element Galois group, the field norm, and its fixed field; they connect the unit-norm obstruction with the involution formulation.

theorem CCDN.quadratic_automorphism_eq_one_or (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] [Algebra.IsSeparable F K] (hd : Module.finrank F K = 2) (σ : Gal(K/F)) (hσ : σ ≠ 1) (τ : Gal(K/F)) : τ = 1 ∨ τ = σ

In a quadratic separable extension with a nontrivial automorphism σ, every automorphism is either the identity or σ.

theorem CCDN.quadratic_automorphism_involutive (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] [Algebra.IsSeparable F K] (hd : Module.finrank F K = 2) (σ : Gal(K/F)) : Function.Involutive ⇑σ

Every automorphism of a quadratic separable extension is an involution.

theorem CCDN.quadratic_norm_eq_mul_conjugate (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] [Algebra.IsSeparable F K] (hd : Module.finrank F K = 2) (σ : Gal(K/F)) (hσ : σ ≠ 1) (x : K) : (algebraMap F K) ((Algebra.norm F) x) = x * σ x

In a quadratic separable extension with nontrivial automorphism σ, the norm of x is x * σ x.