From 24bd3451ff8f9554a42b0aa57ab74250143a4e3a Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Mon, 27 Jul 2026 20:07:02 +0900
Subject: [PATCH 01/15] first commit

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean |  63 +++++
 Mathlib/Algebra/QuadraticAlgebra/Defs.lean  |   4 +
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean | 249 ++++++++++++++++++++
 3 files changed, 316 insertions(+)
 create mode 100644 Mathlib/Algebra/QuadraticAlgebra/Discr.lean

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index 659edf8b3748fa..cc5549fa8f7310 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -69,6 +69,10 @@ theorem omega_mul_omega_eq_add :
     (ω : QuadraticAlgebra R a b) * ω = a • 1 + b • ω := by
   ext <;> simp
 
+@[simp]
+theorem basis_apply_one : (basis a b) 1 = ω := by
+  ext <;> simp [basis]
+
 @[simp]
 theorem omega_mul_mk (x y : R) : (ω : QuadraticAlgebra R a b) * ⟨x, y⟩ = ⟨a * y, x + b * y⟩ := by
   ext <;> simp
@@ -302,6 +306,65 @@ theorem norm_mem_nonZeroDivisors_iff {z : QuadraticAlgebra R a b} :
 
 end norm
 
+section trace
+
+variable [CommRing R]
+
+/-- the trace in a quadratic algebra, as an `R`-linear map. -/
+def trace : QuadraticAlgebra R a b →ₗ[R] R where
+  toFun z := 2 * z.re + b * z.im
+  map_add' z w := by simp only [re_add, im_add]; ring
+  map_smul' r z := by simp only [re_smul, im_smul, RingHom.id_apply, smul_eq_mul]; ring
+
+theorem trace_apply (z : QuadraticAlgebra R a b) :
+    trace z = 2 * z.re + b * z.im := rfl
+
+@[simp]
+theorem trace_algebraMap (r : R) :
+    trace (algebraMap R (QuadraticAlgebra R a b) r) = 2 * r := by
+  simp [trace_apply, algebraMap_re, algebraMap_im]
+
+@[simp]
+theorem trace_natCast (n : ℕ) : trace (n : QuadraticAlgebra R a b) = 2 * n := by
+  simp [trace_apply, re_natCast, im_natCast]
+
+@[simp]
+theorem trace_intCast (n : ℤ) : trace (n : QuadraticAlgebra R a b) = 2 * n := by
+  simp [trace_apply, re_intCast, im_intCast]
+
+@[simp]
+theorem trace_omega : trace (ω : QuadraticAlgebra R a b) = b := by
+  simp [trace_apply]
+
+@[simp]
+theorem trace_one : trace (1 : QuadraticAlgebra R a b) = 2 := by
+  simp [trace_apply]
+
+@[simp]
+theorem trace_star (z : QuadraticAlgebra R a b) : trace (star z) = trace z := by
+  simp only [trace_apply, re_star, im_star]
+  ring
+
+/-- `z + star z` is the trace of `z`. -/
+theorem algebraMap_trace_eq_add_star (z : QuadraticAlgebra R a b) :
+    algebraMap R (QuadraticAlgebra R a b) (trace z) = z + star z := by
+  ext <;>
+  simp only [trace_apply, algebraMap_re, algebraMap_im, re_add, im_add, re_star, im_star] <;>
+  ring
+
+/-- Every element of a quadratic algebra satisfies its characteristic equation. -/
+theorem sq_sub_trace_smul_add_norm_eq_zero (z : QuadraticAlgebra R a b) :
+    z ^ 2 - trace z • z + algebraMap R _ (norm z) = 0 := by
+  rw [Algebra.smul_def, algebraMap_trace_eq_add_star, algebraMap_norm_eq_mul_star]; ring
+
+/-- The reduction `z ^ 2 = trace z • z - norm z`, lowering the degree of a square. -/
+theorem sq_eq_trace_smul_sub_norm (z : QuadraticAlgebra R a b) :
+    z ^ 2 = trace z • z - algebraMap R _ (norm z) := by
+  rw [← sub_eq_zero, ← sub_add]
+  exact sq_sub_trace_smul_add_norm_eq_zero z
+
+end trace
+
 section field
 
 variable [Field K] {a b : K} [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)]
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Defs.lean b/Mathlib/Algebra/QuadraticAlgebra/Defs.lean
index 780ca423edde6b..fb151a36386043 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Defs.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Defs.lean
@@ -382,6 +382,10 @@ noncomputable def basis : Module.Basis (Fin 2) R (QuadraticAlgebra R a b) :=
 theorem basis_repr_apply (x : QuadraticAlgebra R a b) :
     (basis a b).repr x = ![x.re, x.im] := rfl
 
+@[simp]
+theorem basis_apply_zero : (basis a b) 0 = 1 := by
+  ext <;> simp [basis]
+
 instance : Module.Finite R (QuadraticAlgebra R a b) := .of_basis (basis a b)
 
 instance : Module.Free R (QuadraticAlgebra R a b) := .of_basis (basis a b)
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
new file mode 100644
index 00000000000000..e9dc1d0c6423f0
--- /dev/null
+++ b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
@@ -0,0 +1,249 @@
+/-
+Copyright (c) 2026 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+module
+
+public import Mathlib.Algebra.QuadraticAlgebra.Basic
+public import Mathlib.Data.Nat.Prime.Int
+public import Mathlib.LinearAlgebra.Determinant
+
+/-!
+# Discriminant of a quadratic algebra
+
+For `QuadraticAlgebra R a b` (with convention `ω² = a + b·ω`), we define its discriminant
+`discr a b = b ^ 2 + 4 * a`, the discriminant of the polynomial `X ^ 2 - b * X - a`.
+
+We study how the discriminant transforms under a change of generator `ω ↦ u • ω + k`
+(`QuadraticAlgebra.map` / `QuadraticAlgebra.mapEquiv`), showing `discr` is multiplied
+by `u ^ 2`, and deduce that the discriminant classifies quadratic algebras up to isomorphism:
+modulo squares of units when `2` is invertible, and exactly over `ℤ`.
+
+We also characterise, when `2 ≠ 0`, when `QuadraticAlgebra K a b` is a field over a
+field `K`, namely when `discr a b` is not a square.
+
+This is **false in characteristic `2`**: over `𝔽₂` the parameters `(0, 1)` and `(1, 1)` share
+discriminant `1`, yet `X² − X` splits (giving `𝔽₂ × 𝔽₂`) while `X² + X + 1` is irreducible
+(giving `𝔽₄`); the correct invariant there is the Artin–Schreier class.
+
+For `u` not a unit, `map` is the inclusion of an order of conductor `u`, with discriminant
+multiplied by `u ^ 2` (e.g. `ℤ[√d] ⊂ ℤ[(1+√d)/2]` for `d ≡ 1 mod 4` is `u = 2`, `k = -1`).
+Note `discr d 0 = 4 * d`, not `d`, matching the discriminant `4d` of `ℤ[√d]`.
+-/
+
+@[expose] public section
+
+namespace QuadraticAlgebra
+
+variable {R : Type*}
+
+section discr
+
+/-- The discriminant of the quadratic algebra `QuadraticAlgebra R a b`, that is, the
+discriminant `b ^ 2 + 4 * a` of the polynomial `X ^ 2 - b * X - a`. -/
+def discr [CommSemiring R] (a b : R) : R := b ^ 2 + 4 * a
+
+theorem discr_def [CommSemiring R] (a b : R) : discr a b = b ^ 2 + 4 * a := rfl
+
+/-- `z.im ^ 2` times the discriminant of the algebra equals `trace z ^ 2 - 4 * norm z`. -/
+theorem im_sq_mul_discr [CommRing R] {a b : R} (z : QuadraticAlgebra R a b) :
+    z.im ^ 2 * discr a b = trace z ^ 2 - 4 * norm z := by
+  rw [trace_apply, norm_def, discr_def]; ring
+
+-- The `a = 1` case of `Mathlib.Algebra.QuadraticDiscriminant`, reproved to avoid its heavy
+-- transitive import of `Mathlib.Order.Filter.AtTopBot.Field`.
+/-- If `2` is invertible, the polynomial `X ^ 2 - b * X - a` has a root if and only if the
+discriminant is a square. -/
+theorem exists_sq_eq_iff_isSquare_discr [CommRing R] [Invertible (2 : R)] {a b : R} :
+    (∃ r : R, r ^ 2 = a + b * r) ↔ IsSquare (discr a b) := by
+  rw [isSquare_iff_exists_sq]
+  have h2 := mul_invOf_self (2 : R)
+  refine ⟨fun ⟨r, hr⟩ ↦ ⟨2 * r - b, by rw [discr_def]; grind⟩, fun ⟨s, hs⟩ ↦ ⟨⅟2 * (b + s), ?_⟩⟩
+  rw [discr_def] at hs
+  grind
+
+end discr
+
+section map
+
+variable [CommRing R]
+
+-- The quadratic relation satisfied by the new generator `u • ω + k`; this is what makes
+-- `map` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of the
+-- subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds `map` verbatim.
+private theorem map_relation (a b u k : R) :
+    (u • ω + algebraMap R (QuadraticAlgebra R a b) k) *
+        (u • ω + algebraMap R (QuadraticAlgebra R a b) k) =
+      (u ^ 2 * a - u * b * k - k ^ 2) • 1 +
+        (u * b + 2 * k) • (u • ω + algebraMap R (QuadraticAlgebra R a b) k) := by
+  ext <;> simp <;> ring
+
+/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see `map_omega`. -/
+@[simps!]
+def map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) :
+    QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b :=
+  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact map_relation a b u k⟩
+
+@[simp]
+theorem map_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) :
+    map a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
+  ext <;> simp
+
+theorem injective_map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) (hu : IsRegular u) :
+    Function.Injective (map a b u k ha hb) := by
+  intro z w h
+  have hy : z.im = w.im := hu.right <| by simpa using congr_arg im h
+  exact QuadraticAlgebra.ext (by simpa [hy] using congr_arg re h) hy
+
+theorem discr_map (a b u k : R) :
+    discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b := by
+  rw [discr_def, discr_def]
+  ring
+
+/-- `map` along a unit `u`, as an isomorphism. -/
+@[simps! apply symm_apply]
+def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
+    (ha : a' = (u : R) ^ 2 * a - (u : R) * b * k - k ^ 2)
+    (hb : b' = (u : R) * b + 2 * k) :
+    QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b where
+  __ := map a b u k ha hb
+  invFun := map a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
+    (by simp only [sq, ha, mul_assoc, mul_sub, Units.inv_mul_cancel_left, hb, mul_add, neg_mul,
+        mul_neg, sub_neg_eq_add, neg_neg]; ring)
+    (by simp only [hb, mul_add, Units.inv_mul_cancel_left, neg_mul, mul_neg]; ring)
+  left_inv _ := by ext <;> simp [mul_assoc]
+  right_inv _ := by ext <;> simp [mul_assoc]
+
+end map
+
+section classification
+
+variable [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b)
+
+private theorem smul_omega_sub_eq :
+    (trace (f ω) - b') • f ω = algebraMap R _ (norm (f ω)) + a' • 1 := by
+  rw [sub_smul, ← sub_neg_eq_add, sub_eq_sub_iff_sub_eq_sub, ← sq_eq_trace_smul_sub_norm,
+    sub_neg_eq_add, ← map_pow, sq, omega_mul_omega_eq_add, map_add, map_smul, map_smul, map_one,
+    add_comm]
+
+/-- If `(f ω).im` is regular, an algebra map sends `ω` to an element of trace `b'`. -/
+theorem trace_map_omega (h : IsRegular (f ω).im) :
+    trace (f ω) = b' := by
+  simpa [h.right.mul_right_eq_zero_iff, sub_eq_zero] using congr_arg im (smul_omega_sub_eq f)
+
+/-- If `(f ω).im` is regular, an algebra map sends `ω` to an element of norm `-a'`. -/
+theorem norm_map_omega (h : IsRegular (f ω).im) :
+    norm (f ω) = -a' := by
+  simpa [trace_map_omega f h, ← Algebra.algebraMap_eq_smul_one, add_eq_zero_iff_eq_neg,
+    ← map_neg] using (smul_omega_sub_eq f).symm
+
+/-- The transformation law in the case when `(f ω).im` is regular. -/
+theorem discr_eq_im_sq_mul_discr (h : IsRegular (f ω).im) :
+    discr a' b' = (f ω).im ^ 2 * discr a b := by
+  rw [im_sq_mul_discr (f ω), trace_map_omega f h, norm_map_omega f h, discr_def]
+  ring
+
+/-- Any `R`-algebra isomorphism between quadratic algebras sends `ω` to an element
+whose imaginary part is a unit. -/
+theorem isUnit_im_omega_of_algEquiv (e : QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b) :
+    IsUnit (e ω).im := by
+  simpa [Module.Basis.det_apply, Matrix.det_fin_two, Module.Basis.toMatrix_apply] using
+    (basis a b).isUnit_det ((basis a' b').map e.toLinearEquiv)
+
+/-- `discr_eq_im_sq_mul_discr` for an `R`-algebra isomorphism `e`, for which `(e ω).im` is
+automatically a unit (`isUnit_im_omega_of_algEquiv`). -/
+theorem discr_eq_im_sq_mul_discr' (e : QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b) :
+    discr a' b' = (e ω).im ^ 2 * discr a b := by
+  rw [discr_eq_im_sq_mul_discr e.toAlgHom, AlgEquiv.toAlgHom_apply]
+  exact (isUnit_im_omega_of_algEquiv e).isRegular
+
+/-- If `2` is regular, `QuadraticAlgebra R a b` and `QuadraticAlgebra R a' b'` are isomorphic
+iff `discr a b = u ^ 2 * discr a' b'` for some unit `u` with `2 ∣ b - u * b'`. -/
+theorem nonempty_algEquiv_iff (h : IsRegular (2 : R)) :
+    Nonempty (QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R a' b') ↔
+      ∃ u : Rˣ, discr a b = (u : R) ^ 2 * discr a' b' ∧ 2 ∣ (b - u * b') := by
+  refine ⟨fun ⟨e⟩ ↦ ?_, fun ⟨u, hu, ⟨k, hk⟩⟩ ↦ ⟨mapEquiv a' b' u k ?_ (by grind)⟩⟩
+  · refine ⟨(isUnit_im_omega_of_algEquiv e).unit,
+      by rw [discr_eq_im_sq_mul_discr' e, IsUnit.unit_spec], ⟨(e ω).re, ?_⟩⟩
+    rw [IsUnit.unit_spec, sub_eq_iff_eq_add', add_comm, mul_comm _ b', ← trace_apply, eq_comm]
+    exact trace_map_omega e.toAlgHom (isUnit_im_omega_of_algEquiv e).isRegular
+  · rw [discr_def, discr_def] at hu
+    rw [← h.left.eq_iff, mul_sub, mul_sub, ← mul_rotate, ← mul_assoc, ← mul_assoc, ← mul_assoc,
+      ← hk, ← h.left.eq_iff, mul_sub, ← mul_assoc, ← mul_assoc, ← pow_two, ← mul_pow, ← hk]
+    grind
+
+/-- If `2` is invertible, the discriminant classifies quadratic algebras up to
+isomorphism, modulo squares of units. -/
+theorem nonempty_algEquiv_iff_of_invertible_two [Invertible (2 : R)] :
+    Nonempty (QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R a' b') ↔
+      ∃ u : Rˣ, discr a b = (u : R) ^ 2 * discr a' b' := by
+  rw [nonempty_algEquiv_iff (isUnit_of_invertible (2 : R)).isRegular]
+  simp [(isUnit_of_invertible (2 : R)).dvd]
+
+/-- Over `ℤ` the discriminant is a complete invariant of quadratic algebras up to
+isomorphism. -/
+theorem nonempty_algEquiv_int_iff {a b a' b' : ℤ} :
+    Nonempty (QuadraticAlgebra ℤ a b ≃ₐ[ℤ] QuadraticAlgebra ℤ a' b') ↔
+      discr a b = discr a' b' := by
+  rw [nonempty_algEquiv_iff (IsRegular.of_ne_zero two_ne_zero)]
+  refine ⟨fun ⟨u, hu, _⟩ ↦ by rwa [Int.isUnit_sq u.isUnit, one_mul] at hu, fun h ↦ ?_⟩
+  obtain _ | _ : 2 ∣ (b + b') ∨ 2 ∣ (b - b') := by
+    rw [← Prime.dvd_mul (by exact Nat.prime_iff_prime_int.mp Nat.prime_two), ← sq_sub_sq]
+    refine ⟨2 * a' - 2 * a, ?_⟩
+    rwa [mul_sub, ← mul_assoc, ← mul_assoc, show (2 : ℤ) * 2 = 4 by norm_num,
+      sub_eq_sub_iff_add_eq_add, ← discr_def, add_comm, ← discr_def]
+  · exact ⟨-1, by simpa, by simpa⟩
+  · exact ⟨1, by simpa, by simpa⟩
+
+end classification
+
+section field
+
+/-- Bridge instance for `b = 0`: no hypothesis on the characteristic is needed. -/
+instance {K : Type*} [Field K] {a : K} [Fact (¬ IsSquare a)] :
+    Fact (∀ r : K, r ^ 2 ≠ a + 0 * r) :=
+  ⟨fun r hr ↦ Fact.out (p := ¬ IsSquare a) ⟨r, by simpa [sq] using hr.symm⟩⟩
+
+/-- Bridge instance in general, when `2` is invertible. -/
+instance {K : Type*} [Field K] {a b : K} [NeZero (2 : K)] [Fact (¬ IsSquare (discr a b))] :
+    Fact (∀ r : K, r ^ 2 ≠ a + b * r) :=
+  letI : Invertible (2 : K) := invertibleOfNonzero two_ne_zero
+  ⟨not_exists.mp <| exists_sq_eq_iff_isSquare_discr.not.mpr Fact.out⟩
+
+variable {K : Type*} [Field K]
+
+/-- If `discr a b` is a square, `QuadraticAlgebra K a b` is not a field. -/
+theorem not_isField_of_isSquare_discr [NeZero (2 : K)] {a b : K}
+    (h : IsSquare (discr a b)) : ¬ IsField (QuadraticAlgebra K a b) := by
+  let : Invertible (2 : K) := invertibleOfNonzero two_ne_zero
+  obtain ⟨r, hr⟩ := exists_sq_eq_iff_isSquare_discr.mpr h
+  intro hfield
+  let := hfield.toField
+  have : (⟨r, -1⟩ : QuadraticAlgebra K a b) ∈ nonZeroDivisors (QuadraticAlgebra K a b) := by
+    simp [mem_nonZeroDivisors_iff_ne_zero, QuadraticAlgebra.ext_iff]
+  rw [← norm_mem_nonZeroDivisors_iff, show norm ⟨r, -1⟩ = 0 by rw [norm_def]; grind] at this
+  exact zero_notMem_nonZeroDivisors this
+
+/-- If `2 ≠ 0` in the field `K`, `QuadraticAlgebra K a b` is a field iff `discr a b` is
+not a square. -/
+theorem isField_iff_not_isSquare_discr [NeZero (2 : K)] {a b : K} :
+    IsField (QuadraticAlgebra K a b) ↔ ¬ IsSquare (discr a b) := by
+  let : Invertible (2 : K) := invertibleOfNonzero two_ne_zero
+  refine ⟨fun hfield h ↦ not_isField_of_isSquare_discr h hfield, fun h ↦ ?_⟩
+  have : Fact (¬ IsSquare (discr a b)) := ⟨h⟩
+  exact Field.toIsField (QuadraticAlgebra K a b)
+
+-- The `b = 0` bridge makes the `Field` instance inferable from `¬ IsSquare a` alone.
+example {a : K} [Fact (¬ IsSquare a)] : Field (QuadraticAlgebra K a 0) := inferInstance
+
+-- The general bridge makes the `Field` instance inferable from `¬ IsSquare (discr a b)`
+-- if `2 ≠ 0` in the field.
+example {a b : ℚ} [Fact (¬ IsSquare (discr a b))] : Field (QuadraticAlgebra ℚ a b) := inferInstance
+
+end field
+
+end QuadraticAlgebra

From 869ffeef64dae25eeeac592dd7051abce0fc3b38 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Wed, 29 Jul 2026 08:19:45 +0900
Subject: [PATCH 02/15] move maps to Basic

---
 Mathlib.lean                                |   1 +
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean |  59 ++++++++++-
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean | 106 ++++++--------------
 3 files changed, 88 insertions(+), 78 deletions(-)

diff --git a/Mathlib.lean b/Mathlib.lean
index 624f35d65fc813..e6540b456f07cf 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1207,6 +1207,7 @@ public import Mathlib.Algebra.Prime.Defs
 public import Mathlib.Algebra.Prime.Lemmas
 public import Mathlib.Algebra.QuadraticAlgebra.Basic
 public import Mathlib.Algebra.QuadraticAlgebra.Defs
+public import Mathlib.Algebra.QuadraticAlgebra.Discr
 public import Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
 public import Mathlib.Algebra.QuadraticDiscriminant
 public import Mathlib.Algebra.Quandle
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index cc5549fa8f7310..91f686e4f423f0 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -11,7 +11,7 @@ public import Mathlib.Algebra.Star.Unitary
 import Mathlib.Tactic.FieldSimp
 
 /-!
-# Quadratic algebras: involution and norm.
+# Quadratic algebras: involution, norm, trace, and change of generator.
 
 Let `R` be a commutative ring. We define:
 
@@ -19,6 +19,11 @@ Let `R` be a commutative ring. We define:
 
 * `QuadraticAlgebra.norm`: the norm
 
+* `QuadraticAlgebra.trace`: the trace, as an `R`-linear map
+
+* `QuadraticAlgebra.map` and `QuadraticAlgebra.mapEquiv`: the `R`-algebra map, respectively
+  isomorphism (when `u` is a unit), induced by the change of generator `ω ↦ u • ω + k`
+
 We prove:
 
 * `QuadraticAlgebra.isUnit_iff_norm_isUnit`:
@@ -152,7 +157,7 @@ section star
 variable [CommRing R]
 
 /-- Conjugation in `QuadraticAlgebra R a b`.
-The conjugate of `x + y ω` is `x + y ω' = (x - a * y) - y ω`. -/
+The conjugate of `x + y ω` is `x + y ω' = (x + b * y) - y ω`. -/
 instance : Star (QuadraticAlgebra R a b) where
   star z := ⟨z.re + b * z.im, -z.im⟩
 
@@ -365,6 +370,56 @@ theorem sq_eq_trace_smul_sub_norm (z : QuadraticAlgebra R a b) :
 
 end trace
 
+section map
+
+variable [CommRing R]
+
+-- The quadratic relation satisfied by the new generator `u • ω + k`; this is what makes
+-- `map` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of the
+-- subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds `map` verbatim.
+private theorem map_relation (a b u k : R) :
+    (u • ω + algebraMap R (QuadraticAlgebra R a b) k) *
+        (u • ω + algebraMap R (QuadraticAlgebra R a b) k) =
+      (u ^ 2 * a - u * b * k - k ^ 2) • 1 +
+        (u * b + 2 * k) • (u • ω + algebraMap R (QuadraticAlgebra R a b) k) := by
+  ext <;> simp <;> ring
+
+/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see `map_omega`. -/
+@[simps!]
+def map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) :
+    QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b :=
+  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact map_relation a b u k⟩
+
+@[simp]
+theorem map_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) :
+    map a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
+  ext <;> simp
+
+theorem injective_map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) (hu : IsRegular u) :
+    Function.Injective (map a b u k ha hb) := by
+  intro z w h
+  have hy : z.im = w.im := hu.right <| by simpa using congr_arg im h
+  exact QuadraticAlgebra.ext (by simpa [hy] using congr_arg re h) hy
+
+/-- `map` along a unit `u`, as an isomorphism. -/
+@[simps! apply symm_apply]
+def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
+    (ha : a' = (u : R) ^ 2 * a - (u : R) * b * k - k ^ 2)
+    (hb : b' = (u : R) * b + 2 * k) :
+    QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b where
+  __ := map a b u k ha hb
+  invFun := map a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
+    (by simp only [sq, ha, mul_assoc, mul_sub, Units.inv_mul_cancel_left, hb, mul_add, neg_mul,
+        mul_neg, sub_neg_eq_add, neg_neg]; ring)
+    (by simp only [hb, mul_add, Units.inv_mul_cancel_left, neg_mul, mul_neg]; ring)
+  left_inv _ := by ext <;> simp [mul_assoc]
+  right_inv _ := by ext <;> simp [mul_assoc]
+
+end map
+
 section field
 
 variable [Field K] {a b : K} [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)]
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
index e9dc1d0c6423f0..a6d2e19970f4bc 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
@@ -12,24 +12,26 @@ public import Mathlib.LinearAlgebra.Determinant
 /-!
 # Discriminant of a quadratic algebra
 
-For `QuadraticAlgebra R a b` (with convention `ω² = a + b·ω`), we define its discriminant
-`discr a b = b ^ 2 + 4 * a`, the discriminant of the polynomial `X ^ 2 - b * X - a`.
-
-We study how the discriminant transforms under a change of generator `ω ↦ u • ω + k`
-(`QuadraticAlgebra.map` / `QuadraticAlgebra.mapEquiv`), showing `discr` is multiplied
-by `u ^ 2`, and deduce that the discriminant classifies quadratic algebras up to isomorphism:
-modulo squares of units when `2` is invertible, and exactly over `ℤ`.
-
-We also characterise, when `2 ≠ 0`, when `QuadraticAlgebra K a b` is a field over a
-field `K`, namely when `discr a b` is not a square.
-
-This is **false in characteristic `2`**: over `𝔽₂` the parameters `(0, 1)` and `(1, 1)` share
-discriminant `1`, yet `X² − X` splits (giving `𝔽₂ × 𝔽₂`) while `X² + X + 1` is irreducible
-(giving `𝔽₄`); the correct invariant there is the Artin–Schreier class.
-
-For `u` not a unit, `map` is the inclusion of an order of conductor `u`, with discriminant
-multiplied by `u ^ 2` (e.g. `ℤ[√d] ⊂ ℤ[(1+√d)/2]` for `d ≡ 1 mod 4` is `u = 2`, `k = -1`).
-Note `discr d 0 = 4 * d`, not `d`, matching the discriminant `4d` of `ℤ[√d]`.
+This file introduces the discriminant of a quadratic algebra `QuadraticAlgebra R a b` (with the
+convention `ω² = a + b·ω`), describes how it transforms under a change of generator, and derives
+the classification of quadratic algebras up to isomorphism together with a criterion, over a
+field, for `QuadraticAlgebra K a b` to be a field.
+
+## Main definitions
+
+* `QuadraticAlgebra.discr`: the discriminant `discr a b = b ^ 2 + 4 * a`.
+
+## Main results
+
+* `QuadraticAlgebra.discr_map`: the discriminant scales by `u ^ 2` under the change of
+  generator `ω ↦ u • ω + k`.
+* `QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr`: over a ring with `2` invertible,
+  `X ^ 2 - b * X - a` has a root iff `discr a b` is a square.
+* `QuadraticAlgebra.nonempty_algEquiv_iff_of_invertible_two` and
+  `QuadraticAlgebra.nonempty_algEquiv_int_iff`: the discriminant classifies quadratic algebras
+  up to isomorphism, modulo squares of units when `2` is invertible and exactly over `ℤ`.
+* `QuadraticAlgebra.isField_iff_not_isSquare_discr`: over a field with `2 ≠ 0`,
+  `QuadraticAlgebra K a b` is a field iff `discr a b` is not a square.
 -/
 
 @[expose] public section
@@ -51,6 +53,12 @@ theorem im_sq_mul_discr [CommRing R] {a b : R} (z : QuadraticAlgebra R a b) :
     z.im ^ 2 * discr a b = trace z ^ 2 - 4 * norm z := by
   rw [trace_apply, norm_def, discr_def]; ring
 
+/-- Under the change of generator `ω ↦ u • ω + k` (see `QuadraticAlgebra.map`), the
+discriminant is multiplied by `u ^ 2`. -/
+theorem discr_map [CommRing R] (a b u k : R) :
+    discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b := by
+  rw [discr_def, discr_def]; ring
+
 -- The `a = 1` case of `Mathlib.Algebra.QuadraticDiscriminant`, reproved to avoid its heavy
 -- transitive import of `Mathlib.Order.Filter.AtTopBot.Field`.
 /-- If `2` is invertible, the polynomial `X ^ 2 - b * X - a` has a root if and only if the
@@ -65,61 +73,6 @@ theorem exists_sq_eq_iff_isSquare_discr [CommRing R] [Invertible (2 : R)] {a b :
 
 end discr
 
-section map
-
-variable [CommRing R]
-
--- The quadratic relation satisfied by the new generator `u • ω + k`; this is what makes
--- `map` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of the
--- subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds `map` verbatim.
-private theorem map_relation (a b u k : R) :
-    (u • ω + algebraMap R (QuadraticAlgebra R a b) k) *
-        (u • ω + algebraMap R (QuadraticAlgebra R a b) k) =
-      (u ^ 2 * a - u * b * k - k ^ 2) • 1 +
-        (u * b + 2 * k) • (u • ω + algebraMap R (QuadraticAlgebra R a b) k) := by
-  ext <;> simp <;> ring
-
-/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see `map_omega`. -/
-@[simps!]
-def map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
-    (hb : b' = u * b + 2 * k) :
-    QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b :=
-  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact map_relation a b u k⟩
-
-@[simp]
-theorem map_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
-    (hb : b' = u * b + 2 * k) :
-    map a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
-  ext <;> simp
-
-theorem injective_map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
-    (hb : b' = u * b + 2 * k) (hu : IsRegular u) :
-    Function.Injective (map a b u k ha hb) := by
-  intro z w h
-  have hy : z.im = w.im := hu.right <| by simpa using congr_arg im h
-  exact QuadraticAlgebra.ext (by simpa [hy] using congr_arg re h) hy
-
-theorem discr_map (a b u k : R) :
-    discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b := by
-  rw [discr_def, discr_def]
-  ring
-
-/-- `map` along a unit `u`, as an isomorphism. -/
-@[simps! apply symm_apply]
-def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
-    (ha : a' = (u : R) ^ 2 * a - (u : R) * b * k - k ^ 2)
-    (hb : b' = (u : R) * b + 2 * k) :
-    QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b where
-  __ := map a b u k ha hb
-  invFun := map a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
-    (by simp only [sq, ha, mul_assoc, mul_sub, Units.inv_mul_cancel_left, hb, mul_add, neg_mul,
-        mul_neg, sub_neg_eq_add, neg_neg]; ring)
-    (by simp only [hb, mul_add, Units.inv_mul_cancel_left, neg_mul, mul_neg]; ring)
-  left_inv _ := by ext <;> simp [mul_assoc]
-  right_inv _ := by ext <;> simp [mul_assoc]
-
-end map
-
 section classification
 
 variable [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b)
@@ -192,7 +145,7 @@ theorem nonempty_algEquiv_int_iff {a b a' b' : ℤ} :
   rw [nonempty_algEquiv_iff (IsRegular.of_ne_zero two_ne_zero)]
   refine ⟨fun ⟨u, hu, _⟩ ↦ by rwa [Int.isUnit_sq u.isUnit, one_mul] at hu, fun h ↦ ?_⟩
   obtain _ | _ : 2 ∣ (b + b') ∨ 2 ∣ (b - b') := by
-    rw [← Prime.dvd_mul (by exact Nat.prime_iff_prime_int.mp Nat.prime_two), ← sq_sub_sq]
+    rw [← Prime.dvd_mul Int.prime_two, ← sq_sub_sq]
     refine ⟨2 * a' - 2 * a, ?_⟩
     rwa [mul_sub, ← mul_assoc, ← mul_assoc, show (2 : ℤ) * 2 = 4 by norm_num,
       sub_eq_sub_iff_add_eq_add, ← discr_def, add_comm, ← discr_def]
@@ -203,12 +156,13 @@ end classification
 
 section field
 
-/-- Bridge instance for `b = 0`: no hypothesis on the characteristic is needed. -/
+-- These two `Fact (∀ r, r ^ 2 ≠ …)` instances are the bridge that lets the `Field`
+-- instance on `QuadraticAlgebra K a b` fire from `¬ IsSquare (discr a b)` (or `¬ IsSquare a`
+-- when `b = 0`) alone.
 instance {K : Type*} [Field K] {a : K} [Fact (¬ IsSquare a)] :
     Fact (∀ r : K, r ^ 2 ≠ a + 0 * r) :=
   ⟨fun r hr ↦ Fact.out (p := ¬ IsSquare a) ⟨r, by simpa [sq] using hr.symm⟩⟩
 
-/-- Bridge instance in general, when `2` is invertible. -/
 instance {K : Type*} [Field K] {a b : K} [NeZero (2 : K)] [Fact (¬ IsSquare (discr a b))] :
     Fact (∀ r : K, r ^ 2 ≠ a + b * r) :=
   letI : Invertible (2 : K) := invertibleOfNonzero two_ne_zero

From 5de3830660ecfe257f5a931530b71d135144f1e9 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Wed, 29 Jul 2026 10:21:58 +0900
Subject: [PATCH 03/15] first commit

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 55 ++++++++++++++++++++-
 1 file changed, 54 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index 659edf8b3748fa..df7587cf26e2d5 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -11,7 +11,7 @@ public import Mathlib.Algebra.Star.Unitary
 import Mathlib.Tactic.FieldSimp
 
 /-!
-# Quadratic algebras: involution and norm.
+# Quadratic algebras: involution, norm, and change of generator.
 
 Let `R` be a commutative ring. We define:
 
@@ -19,6 +19,9 @@ Let `R` be a commutative ring. We define:
 
 * `QuadraticAlgebra.norm`: the norm
 
+* `QuadraticAlgebra.map` and `QuadraticAlgebra.mapEquiv`: the `R`-algebra map, respectively
+  isomorphism (when `u` is a unit), induced by the change of generator `ω ↦ u • ω + k`
+
 We prove:
 
 * `QuadraticAlgebra.isUnit_iff_norm_isUnit`:
@@ -302,6 +305,56 @@ theorem norm_mem_nonZeroDivisors_iff {z : QuadraticAlgebra R a b} :
 
 end norm
 
+section map
+
+variable [CommRing R]
+
+-- The quadratic relation satisfied by the new generator `u • ω + k`; this is what makes
+-- `map` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of the
+-- subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds `map` verbatim.
+private theorem map_relation (a b u k : R) :
+    (u • ω + algebraMap R (QuadraticAlgebra R a b) k) *
+        (u • ω + algebraMap R (QuadraticAlgebra R a b) k) =
+      (u ^ 2 * a - u * b * k - k ^ 2) • 1 +
+        (u * b + 2 * k) • (u • ω + algebraMap R (QuadraticAlgebra R a b) k) := by
+  ext <;> simp <;> ring
+
+/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see `map_omega`. -/
+@[simps!]
+def map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) :
+    QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b :=
+  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact map_relation a b u k⟩
+
+@[simp]
+theorem map_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) :
+    map a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
+  ext <;> simp
+
+theorem map_injective (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) (hu : IsRegular u) :
+    Function.Injective (map a b u k ha hb) := by
+  intro z w h
+  have hy : z.im = w.im := hu.right <| by simpa using congr_arg im h
+  exact QuadraticAlgebra.ext (by simpa [hy] using congr_arg re h) hy
+
+/-- `map` along a unit `u`, as an isomorphism. -/
+@[simps! apply symm_apply]
+def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
+    (ha : a' = (u : R) ^ 2 * a - (u : R) * b * k - k ^ 2)
+    (hb : b' = (u : R) * b + 2 * k) :
+    QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b where
+  __ := map a b u k ha hb
+  invFun := map a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
+    (by simp only [sq, ha, mul_assoc, mul_sub, Units.inv_mul_cancel_left, hb, mul_add, neg_mul,
+        mul_neg, sub_neg_eq_add, neg_neg]; ring)
+    (by simp only [hb, mul_add, Units.inv_mul_cancel_left, neg_mul, mul_neg]; ring)
+  left_inv _ := by ext <;> simp [mul_assoc]
+  right_inv _ := by ext <;> simp [mul_assoc]
+
+end map
+
 section field
 
 variable [Field K] {a b : K} [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)]

From 1c2291fd08a9ba6273a74837ad15ca9e5d8ae5e4 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Wed, 29 Jul 2026 11:12:30 +0900
Subject: [PATCH 04/15] add lemma

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 10 ++++++++
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean | 27 +++++++++++++++++++++
 2 files changed, 37 insertions(+)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index 91f686e4f423f0..58c5d02d06f484 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -357,6 +357,16 @@ theorem algebraMap_trace_eq_add_star (z : QuadraticAlgebra R a b) :
   simp only [trace_apply, algebraMap_re, algebraMap_im, re_add, im_add, re_star, im_star] <;>
   ring
 
+/-- The conjugate of `z` is `trace z - z`. -/
+theorem star_eq (z : QuadraticAlgebra R a b) :
+    star z = algebraMap R (QuadraticAlgebra R a b) (trace z) - z := by
+  rw [algebraMap_trace_eq_add_star]; ring
+
+/-- `z - star z` is a multiple of the different `ω - star ω`. -/
+theorem sub_star (z : QuadraticAlgebra R a b) :
+    z - star z = z.im • (ω - star ω) := by
+  ext <;> simp <;> ring
+
 /-- Every element of a quadratic algebra satisfies its characteristic equation. -/
 theorem sq_sub_trace_smul_add_norm_eq_zero (z : QuadraticAlgebra R a b) :
     z ^ 2 - trace z • z + algebraMap R _ (norm z) = 0 := by
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
index a6d2e19970f4bc..41a8bca0ae183a 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
@@ -59,6 +59,11 @@ theorem discr_map [CommRing R] (a b u k : R) :
     discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b := by
   rw [discr_def, discr_def]; ring
 
+/-- The discriminant is the square of the different `ω - star ω`. -/
+theorem algebraMap_discr [CommRing R] (a b : R) :
+    algebraMap R (QuadraticAlgebra R a b) (discr a b) = (ω - star ω) ^ 2 := by
+  rw [discr_def]; ext <;> simp [sq] <;> ring
+
 -- The `a = 1` case of `Mathlib.Algebra.QuadraticDiscriminant`, reproved to avoid its heavy
 -- transitive import of `Mathlib.Order.Filter.AtTopBot.Field`.
 /-- If `2` is invertible, the polynomial `X ^ 2 - b * X - a` has a root if and only if the
@@ -94,6 +99,28 @@ theorem norm_map_omega (h : IsRegular (f ω).im) :
   simpa [trace_map_omega f h, ← Algebra.algebraMap_eq_smul_one, add_eq_zero_iff_eq_neg,
     ← map_neg] using (smul_omega_sub_eq f).symm
 
+/-- If `(f ω).im` is regular, an algebra map commutes with conjugation. -/
+theorem map_star (h : IsRegular (f ω).im) (x : QuadraticAlgebra R a' b') :
+    f (star x) = star (f x) := by
+  have hs : ∀ {c d : R} (r : R) (y : QuadraticAlgebra R c d), star (r • y) = r • star y := by
+    intro c d r y; ext <;> simp only [re_star, im_star, re_smul, im_smul, smul_eq_mul] <;> ring
+  have ha : ∀ {c d : R} (r : R),
+      star (algebraMap R (QuadraticAlgebra R c d) r) = algebraMap R _ r := by
+    intro c d r; ext <;> simp
+  have homega : f (star ω) = star (f ω) := by
+    rw [star_eq, map_sub, AlgHom.commutes, star_eq (f ω), trace_map_omega f h, trace_omega]
+  rw [← mk_eta x, mk_eq_add_smul_omega]
+  simp only [star_add, ha, hs, map_add, map_smul, AlgHom.commutes, homega]
+
+/-- If `(f ω).im` is regular, an algebra map preserves traces. -/
+theorem trace_map (h : IsRegular (f ω).im) (x : QuadraticAlgebra R a' b') :
+    trace (f x) = trace x := by
+  have key : algebraMap R (QuadraticAlgebra R a b) (trace (f x)) =
+      algebraMap R (QuadraticAlgebra R a b) (trace x) := by
+    rw [algebraMap_trace_eq_add_star, ← AlgHom.commutes f (trace x),
+      algebraMap_trace_eq_add_star, map_add, map_star f h]
+  simpa using congr_arg re key
+
 /-- The transformation law in the case when `(f ω).im` is regular. -/
 theorem discr_eq_im_sq_mul_discr (h : IsRegular (f ω).im) :
     discr a' b' = (f ω).im ^ 2 * discr a b := by

From 1090f395ed404a6ff7c60817537fdb5230b52b93 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Sat, 1 Aug 2026 08:50:10 +0900
Subject: [PATCH 05/15] fix after merge

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 100 ++++++++++----------
 1 file changed, 50 insertions(+), 50 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index a056c909d44eeb..fbcd1a17a8432e 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -312,56 +312,6 @@ theorem norm_mem_nonZeroDivisors_iff {z : QuadraticAlgebra R a b} :
 
 end norm
 
-section map
-
-variable [CommRing R]
-
--- The quadratic relation satisfied by the new generator `u • ω + k`; this is what makes
--- `map` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of the
--- subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds `map` verbatim.
-private theorem map_relation (a b u k : R) :
-    (u • ω + algebraMap R (QuadraticAlgebra R a b) k) *
-        (u • ω + algebraMap R (QuadraticAlgebra R a b) k) =
-      (u ^ 2 * a - u * b * k - k ^ 2) • 1 +
-        (u * b + 2 * k) • (u • ω + algebraMap R (QuadraticAlgebra R a b) k) := by
-  ext <;> simp <;> ring
-
-/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see `map_omega`. -/
-@[simps!]
-def map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
-    (hb : b' = u * b + 2 * k) :
-    QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b :=
-  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact map_relation a b u k⟩
-
-@[simp]
-theorem map_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
-    (hb : b' = u * b + 2 * k) :
-    map a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
-  ext <;> simp
-
-theorem map_injective (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
-    (hb : b' = u * b + 2 * k) (hu : IsRegular u) :
-    Function.Injective (map a b u k ha hb) := by
-  intro z w h
-  have hy : z.im = w.im := hu.right <| by simpa using congr_arg im h
-  exact QuadraticAlgebra.ext (by simpa [hy] using congr_arg re h) hy
-
-/-- `map` along a unit `u`, as an isomorphism. -/
-@[simps! apply symm_apply]
-def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
-    (ha : a' = (u : R) ^ 2 * a - (u : R) * b * k - k ^ 2)
-    (hb : b' = (u : R) * b + 2 * k) :
-    QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b where
-  __ := map a b u k ha hb
-  invFun := map a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
-    (by simp only [sq, ha, mul_assoc, mul_sub, Units.inv_mul_cancel_left, hb, mul_add, neg_mul,
-        mul_neg, sub_neg_eq_add, neg_neg]; ring)
-    (by simp only [hb, mul_add, Units.inv_mul_cancel_left, neg_mul, mul_neg]; ring)
-  left_inv _ := by ext <;> simp [mul_assoc]
-  right_inv _ := by ext <;> simp [mul_assoc]
-
-end map
-
 section trace
 
 variable [CommRing R]
@@ -425,6 +375,56 @@ theorem sq_eq_trace_smul_sub_norm :
 
 end trace
 
+section map
+
+variable [CommRing R]
+
+-- The quadratic relation satisfied by the new generator `u • ω + k`; this is what makes
+-- `map` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of the
+-- subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds `map` verbatim.
+private theorem map_relation (a b u k : R) :
+    (u • ω + algebraMap R (QuadraticAlgebra R a b) k) *
+        (u • ω + algebraMap R (QuadraticAlgebra R a b) k) =
+      (u ^ 2 * a - u * b * k - k ^ 2) • 1 +
+        (u * b + 2 * k) • (u • ω + algebraMap R (QuadraticAlgebra R a b) k) := by
+  ext <;> simp <;> ring
+
+/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see `map_omega`. -/
+@[simps!]
+def map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) :
+    QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b :=
+  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact map_relation a b u k⟩
+
+@[simp]
+theorem map_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) :
+    map a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
+  ext <;> simp
+
+theorem map_injective (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+    (hb : b' = u * b + 2 * k) (hu : IsRegular u) :
+    Function.Injective (map a b u k ha hb) := by
+  intro z w h
+  have hy : z.im = w.im := hu.right <| by simpa using congr_arg im h
+  exact QuadraticAlgebra.ext (by simpa [hy] using congr_arg re h) hy
+
+/-- `map` along a unit `u`, as an isomorphism. -/
+@[simps! apply symm_apply]
+def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
+    (ha : a' = (u : R) ^ 2 * a - (u : R) * b * k - k ^ 2)
+    (hb : b' = (u : R) * b + 2 * k) :
+    QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b where
+  __ := map a b u k ha hb
+  invFun := map a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
+    (by simp only [sq, ha, mul_assoc, mul_sub, Units.inv_mul_cancel_left, hb, mul_add, neg_mul,
+        mul_neg, sub_neg_eq_add, neg_neg]; ring)
+    (by simp only [hb, mul_add, Units.inv_mul_cancel_left, neg_mul, mul_neg]; ring)
+  left_inv _ := by ext <;> simp [mul_assoc]
+  right_inv _ := by ext <;> simp [mul_assoc]
+
+end map
+
 section field
 
 variable [Field K] {a b : K} [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)]

From 2f9eeff7f7eb9b7bcba4e743445ecafee9060839 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Sun, 2 Aug 2026 17:35:47 +0900
Subject: [PATCH 06/15] add algEquivDiscrZero

---
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
index c6ea2e13bdb855..b1e068a2e3751b 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
@@ -141,6 +141,13 @@ theorem discr_eq_im_sq_mul_discr' (e : QuadraticAlgebra R a' b' ≃ₐ[R] Quadra
   rw [discr_eq_im_sq_mul_discr e.toAlgHom, AlgEquiv.toAlgHom_apply]
   exact (isUnit_im_omega_of_algEquiv e).isRegular
 
+/-- If `2` is a unit, `QuadraticAlgebra R a b` is isomorphic to the standard form
+`QuadraticAlgebra R (discr a b) 0`. -/
+def algEquivDiscrZero [Invertible (2 : R)] (a b : R) :
+    QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R (discr a b) 0 :=
+  (mapEquiv a b (unitOfInvertible (2 : R)) (-b) (by grind [discr_def, val_unitOfInvertible])
+    (by grind [val_unitOfInvertible])).symm
+
 /-- If `2` is regular, `QuadraticAlgebra R a b` and `QuadraticAlgebra R a' b'` are isomorphic
 iff `discr a b = u ^ 2 * discr a' b'` for some unit `u` with `2 ∣ b - u * b'`. -/
 theorem nonempty_algEquiv_iff (h : IsRegular (2 : R)) :

From 636c8e50d527bb6d8a533691402b1d99224b636d Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 13 Aug 2026 09:40:13 +0900
Subject: [PATCH 07/15] rename

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Pxa1HLgwZQg6sssxyFg2o1
---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index e39c474ae17692..75141e7c9ef6b2 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -56,13 +56,16 @@ def omega : QuadraticAlgebra R a b :=
 scoped notation "ω" => omega
 
 @[simp]
-theorem omega_re : (ω : QuadraticAlgebra R a b).re = 0 :=
+theorem re_omega : (ω : QuadraticAlgebra R a b).re = 0 :=
   rfl
 
 @[simp]
-theorem omega_im : (ω : QuadraticAlgebra R a b).im = 1 :=
+theorem im_omega : (ω : QuadraticAlgebra R a b).im = 1 :=
   rfl
 
+@[deprecated (since := "2026-08-13")] alias omega_re := re_omega
+@[deprecated (since := "2026-08-13")] alias omega_im := im_omega
+
 end
 
 variable [CommSemiring R]

From 1c92514e8b96eff5bcad34eb54f60f1dd378baf7 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 13 Aug 2026 09:50:06 +0900
Subject: [PATCH 08/15] split

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Pxa1HLgwZQg6sssxyFg2o1
---
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean | 120 +-------------------
 1 file changed, 2 insertions(+), 118 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
index b1e068a2e3751b..d2be72b31268eb 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
@@ -6,16 +6,13 @@ Authors: Xavier Roblot
 module
 
 public import Mathlib.Algebra.QuadraticAlgebra.Basic
-public import Mathlib.Data.Nat.Prime.Int
-public import Mathlib.LinearAlgebra.Determinant
 
 /-!
 # Discriminant of a quadratic algebra
 
 This file introduces the discriminant of a quadratic algebra `QuadraticAlgebra R a b` (with the
-convention `ω² = a + b·ω`), describes how it transforms under a change of generator, and derives
-the classification of quadratic algebras up to isomorphism together with a criterion, over a
-field, for `QuadraticAlgebra K a b` to be a field.
+convention `ω² = a + b·ω`), describes how it transforms under a change of generator, and derives,
+over a field, a criterion for `QuadraticAlgebra K a b` to be a field.
 
 ## Main definitions
 
@@ -27,9 +24,6 @@ field, for `QuadraticAlgebra K a b` to be a field.
   generator `ω ↦ u • ω + k`.
 * `QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr`: over a ring with `2` invertible,
   `X ^ 2 - b * X - a` has a root iff `discr a b` is a square.
-* `QuadraticAlgebra.nonempty_algEquiv_iff_of_invertible_two` and
-  `QuadraticAlgebra.nonempty_algEquiv_int_iff`: the discriminant classifies quadratic algebras
-  up to isomorphism, modulo squares of units when `2` is invertible and exactly over `ℤ`.
 * `QuadraticAlgebra.isField_iff_not_isSquare_discr`: over a field with `2 ≠ 0`,
   `QuadraticAlgebra K a b` is a field iff `discr a b` is not a square.
 -/
@@ -78,116 +72,6 @@ theorem exists_sq_eq_iff_isSquare_discr [CommRing R] [Invertible (2 : R)] {a b :
 
 end discr
 
-section classification
-
-variable [CommRing R] {a b a' b' : R} (f : QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b)
-
-private theorem smul_omega_sub_eq :
-    (trace (f ω) - b') • f ω = algebraMap R _ (norm (f ω)) + a' • 1 := by
-  rw [sub_smul, ← sub_neg_eq_add, sub_eq_sub_iff_sub_eq_sub, ← sq_eq_trace_smul_sub_norm,
-    sub_neg_eq_add, ← map_pow, sq, omega_mul_omega_eq_add, map_add, map_smul, map_smul, map_one,
-    add_comm]
-
-/-- If `(f ω).im` is regular, an algebra map sends `ω` to an element of trace `b'`. -/
-theorem trace_map_omega (h : IsRegular (f ω).im) :
-    trace (f ω) = b' := by
-  simpa [h.right.mul_right_eq_zero_iff, sub_eq_zero] using congr_arg im (smul_omega_sub_eq f)
-
-/-- If `(f ω).im` is regular, an algebra map sends `ω` to an element of norm `-a'`. -/
-theorem norm_map_omega (h : IsRegular (f ω).im) :
-    norm (f ω) = -a' := by
-  simpa [trace_map_omega f h, ← Algebra.algebraMap_eq_smul_one, add_eq_zero_iff_eq_neg,
-    ← map_neg] using (smul_omega_sub_eq f).symm
-
-/-- If `(f ω).im` is regular, an algebra map commutes with conjugation. -/
-theorem map_star (h : IsRegular (f ω).im) (x : QuadraticAlgebra R a' b') :
-    f (star x) = star (f x) := by
-  have hs : ∀ {c d : R} (r : R) (y : QuadraticAlgebra R c d), star (r • y) = r • star y := by
-    intro c d r y; ext <;> simp only [re_star, im_star, re_smul, im_smul, smul_eq_mul] <;> ring
-  have ha : ∀ {c d : R} (r : R),
-      star (algebraMap R (QuadraticAlgebra R c d) r) = algebraMap R _ r := by
-    intro c d r; ext <;> simp
-  have homega : f (star ω) = star (f ω) := by
-    rw [star_eq, map_sub, AlgHom.commutes, star_eq (f ω), trace_map_omega f h, trace_omega]
-  rw [← mk_eta x, mk_eq_add_smul_omega]
-  simp only [star_add, ha, hs, map_add, map_smul, AlgHom.commutes, homega]
-
-/-- If `(f ω).im` is regular, an algebra map preserves traces. -/
-theorem trace_map (h : IsRegular (f ω).im) (x : QuadraticAlgebra R a' b') :
-    trace (f x) = trace x := by
-  have key : algebraMap R (QuadraticAlgebra R a b) (trace (f x)) =
-      algebraMap R (QuadraticAlgebra R a b) (trace x) := by
-    rw [algebraMap_trace_eq_add_star, ← AlgHom.commutes f (trace x),
-      algebraMap_trace_eq_add_star, map_add, map_star f h]
-  simpa using congr_arg re key
-
-/-- The transformation law in the case when `(f ω).im` is regular. -/
-theorem discr_eq_im_sq_mul_discr (h : IsRegular (f ω).im) :
-    discr a' b' = (f ω).im ^ 2 * discr a b := by
-  rw [im_sq_mul_discr (f ω), trace_map_omega f h, norm_map_omega f h, discr_def]
-  ring
-
-/-- Any `R`-algebra isomorphism between quadratic algebras sends `ω` to an element
-whose imaginary part is a unit. -/
-theorem isUnit_im_omega_of_algEquiv (e : QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b) :
-    IsUnit (e ω).im := by
-  simpa [Module.Basis.det_apply, Matrix.det_fin_two, Module.Basis.toMatrix_apply] using
-    (basis a b).isUnit_det ((basis a' b').map e.toLinearEquiv)
-
-/-- `discr_eq_im_sq_mul_discr` for an `R`-algebra isomorphism `e`, for which `(e ω).im` is
-automatically a unit (`isUnit_im_omega_of_algEquiv`). -/
-theorem discr_eq_im_sq_mul_discr' (e : QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b) :
-    discr a' b' = (e ω).im ^ 2 * discr a b := by
-  rw [discr_eq_im_sq_mul_discr e.toAlgHom, AlgEquiv.toAlgHom_apply]
-  exact (isUnit_im_omega_of_algEquiv e).isRegular
-
-/-- If `2` is a unit, `QuadraticAlgebra R a b` is isomorphic to the standard form
-`QuadraticAlgebra R (discr a b) 0`. -/
-def algEquivDiscrZero [Invertible (2 : R)] (a b : R) :
-    QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R (discr a b) 0 :=
-  (mapEquiv a b (unitOfInvertible (2 : R)) (-b) (by grind [discr_def, val_unitOfInvertible])
-    (by grind [val_unitOfInvertible])).symm
-
-/-- If `2` is regular, `QuadraticAlgebra R a b` and `QuadraticAlgebra R a' b'` are isomorphic
-iff `discr a b = u ^ 2 * discr a' b'` for some unit `u` with `2 ∣ b - u * b'`. -/
-theorem nonempty_algEquiv_iff (h : IsRegular (2 : R)) :
-    Nonempty (QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R a' b') ↔
-      ∃ u : Rˣ, discr a b = (u : R) ^ 2 * discr a' b' ∧ 2 ∣ (b - u * b') := by
-  refine ⟨fun ⟨e⟩ ↦ ?_, fun ⟨u, hu, ⟨k, hk⟩⟩ ↦ ⟨mapEquiv a' b' u k ?_ (by grind)⟩⟩
-  · refine ⟨(isUnit_im_omega_of_algEquiv e).unit,
-      by rw [discr_eq_im_sq_mul_discr' e, IsUnit.unit_spec], ⟨(e ω).re, ?_⟩⟩
-    rw [IsUnit.unit_spec, sub_eq_iff_eq_add', add_comm, mul_comm _ b', ← trace_def, eq_comm]
-    exact trace_map_omega e.toAlgHom (isUnit_im_omega_of_algEquiv e).isRegular
-  · rw [discr_def, discr_def] at hu
-    rw [← h.left.eq_iff, mul_sub, mul_sub, ← mul_rotate, ← mul_assoc, ← mul_assoc, ← mul_assoc,
-      ← hk, ← h.left.eq_iff, mul_sub, ← mul_assoc, ← mul_assoc, ← pow_two, ← mul_pow, ← hk]
-    grind
-
-/-- If `2` is invertible, the discriminant classifies quadratic algebras up to
-isomorphism, modulo squares of units. -/
-theorem nonempty_algEquiv_iff_of_invertible_two [Invertible (2 : R)] :
-    Nonempty (QuadraticAlgebra R a b ≃ₐ[R] QuadraticAlgebra R a' b') ↔
-      ∃ u : Rˣ, discr a b = (u : R) ^ 2 * discr a' b' := by
-  rw [nonempty_algEquiv_iff (isUnit_of_invertible (2 : R)).isRegular]
-  simp [(isUnit_of_invertible (2 : R)).dvd]
-
-/-- Over `ℤ` the discriminant is a complete invariant of quadratic algebras up to
-isomorphism. -/
-theorem nonempty_algEquiv_int_iff {a b a' b' : ℤ} :
-    Nonempty (QuadraticAlgebra ℤ a b ≃ₐ[ℤ] QuadraticAlgebra ℤ a' b') ↔
-      discr a b = discr a' b' := by
-  rw [nonempty_algEquiv_iff (IsRegular.of_ne_zero two_ne_zero)]
-  refine ⟨fun ⟨u, hu, _⟩ ↦ by rwa [Int.isUnit_sq u.isUnit, one_mul] at hu, fun h ↦ ?_⟩
-  obtain _ | _ : 2 ∣ (b + b') ∨ 2 ∣ (b - b') := by
-    rw [← Prime.dvd_mul Int.prime_two, ← sq_sub_sq]
-    refine ⟨2 * a' - 2 * a, ?_⟩
-    rwa [mul_sub, ← mul_assoc, ← mul_assoc, show (2 : ℤ) * 2 = 4 by norm_num,
-      sub_eq_sub_iff_add_eq_add, ← discr_def, add_comm, ← discr_def]
-  · exact ⟨-1, by simpa, by simpa⟩
-  · exact ⟨1, by simpa, by simpa⟩
-
-end classification
-
 section field
 
 -- These two `Fact (∀ r, r ^ 2 ≠ …)` instances are the bridge that lets the `Field`

From 638a69b836fcae65249c76893d38c3f218777e99 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 13 Aug 2026 10:49:47 +0900
Subject: [PATCH 09/15] clean up

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 4 ----
 Mathlib/Algebra/QuadraticAlgebra/Defs.lean  | 4 ----
 2 files changed, 8 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index 75141e7c9ef6b2..43655a0389eef2 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -81,10 +81,6 @@ theorem omega_mul_omega_eq_algebraMap :
     (ω : QuadraticAlgebra R a b) * ω = algebraMap R _ a + algebraMap R _ b * ω := by
   simp [omega_mul_omega_eq_add, Algebra.algebraMap_eq_smul_one]
 
-@[simp]
-theorem basis_apply_one : (basis a b) 1 = ω := by
-  ext <;> simp [basis]
-
 @[simp]
 theorem omega_mul_mk (x y : R) : (ω : QuadraticAlgebra R a b) * ⟨x, y⟩ = ⟨a * y, x + b * y⟩ := by
   ext <;> simp
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Defs.lean b/Mathlib/Algebra/QuadraticAlgebra/Defs.lean
index fb151a36386043..780ca423edde6b 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Defs.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Defs.lean
@@ -382,10 +382,6 @@ noncomputable def basis : Module.Basis (Fin 2) R (QuadraticAlgebra R a b) :=
 theorem basis_repr_apply (x : QuadraticAlgebra R a b) :
     (basis a b).repr x = ![x.re, x.im] := rfl
 
-@[simp]
-theorem basis_apply_zero : (basis a b) 0 = 1 := by
-  ext <;> simp [basis]
-
 instance : Module.Finite R (QuadraticAlgebra R a b) := .of_basis (basis a b)
 
 instance : Module.Free R (QuadraticAlgebra R a b) := .of_basis (basis a b)

From 78f45e1742d060ce0c347918481871e8271122f9 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 13 Aug 2026 11:05:03 +0900
Subject: [PATCH 10/15] clean up

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean |  8 ++++++++
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean | 18 +++---------------
 2 files changed, 11 insertions(+), 15 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index 43655a0389eef2..bd535f35467d04 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -472,6 +472,14 @@ instance : Field (QuadraticAlgebra K a b) where
   nnqsmul_def q x := by ext <;> simp [NNRat.smul_def]
   qsmul_def q x := by ext <;> simp [Rat.smul_def]
 
+/-- When `b = 0`, the `Field` instance is inferable from `¬ IsSquare a` alone: it provides the
+no-root condition `∀ r, r ^ 2 ≠ a + 0 * r`. -/
+instance {a : K} [Fact (¬ IsSquare a)] : Fact (∀ r : K, r ^ 2 ≠ a + 0 * r) :=
+  ⟨fun r hr ↦ Fact.out (p := ¬ IsSquare a) ⟨r, by simpa [sq] using hr.symm⟩⟩
+
+-- The `b = 0` bridge makes the `Field` instance inferable from `¬ IsSquare a` alone.
+example {a : K} [Fact (¬ IsSquare a)] : Field (QuadraticAlgebra K a 0) := inferInstance
+
 end field
 
 end QuadraticAlgebra
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
index d2be72b31268eb..536b5cb1afccee 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
@@ -42,11 +42,6 @@ def discr [CommSemiring R] (a b : R) : R := b ^ 2 + 4 * a
 
 theorem discr_def [CommSemiring R] (a b : R) : discr a b = b ^ 2 + 4 * a := rfl
 
-/-- `z.im ^ 2` times the discriminant of the algebra equals `trace z ^ 2 - 4 * norm z`. -/
-theorem im_sq_mul_discr [CommRing R] {a b : R} (z : QuadraticAlgebra R a b) :
-    z.im ^ 2 * discr a b = trace z ^ 2 - 4 * norm z := by
-  rw [trace_def, norm_def, discr_def]; ring
-
 /-- Under the change of generator `ω ↦ u • ω + k` (see `QuadraticAlgebra.map`), the
 discriminant is multiplied by `u ^ 2`. -/
 theorem discr_map [CommRing R] (a b u k : R) :
@@ -74,13 +69,9 @@ end discr
 
 section field
 
--- These two `Fact (∀ r, r ^ 2 ≠ …)` instances are the bridge that lets the `Field`
--- instance on `QuadraticAlgebra K a b` fire from `¬ IsSquare (discr a b)` (or `¬ IsSquare a`
--- when `b = 0`) alone.
-instance {K : Type*} [Field K] {a : K} [Fact (¬ IsSquare a)] :
-    Fact (∀ r : K, r ^ 2 ≠ a + 0 * r) :=
-  ⟨fun r hr ↦ Fact.out (p := ¬ IsSquare a) ⟨r, by simpa [sq] using hr.symm⟩⟩
-
+-- This `Fact (∀ r, r ^ 2 ≠ …)` instance is the bridge that lets the `Field` instance on
+-- `QuadraticAlgebra K a b` fire from `¬ IsSquare (discr a b)` alone (the `b = 0` bridge from
+-- `¬ IsSquare a` lives in `Basic.lean`).
 instance {K : Type*} [Field K] {a b : K} [NeZero (2 : K)] [Fact (¬ IsSquare (discr a b))] :
     Fact (∀ r : K, r ^ 2 ≠ a + b * r) :=
   letI : Invertible (2 : K) := invertibleOfNonzero two_ne_zero
@@ -109,9 +100,6 @@ theorem isField_iff_not_isSquare_discr [NeZero (2 : K)] {a b : K} :
   have : Fact (¬ IsSquare (discr a b)) := ⟨h⟩
   exact Field.toIsField (QuadraticAlgebra K a b)
 
--- The `b = 0` bridge makes the `Field` instance inferable from `¬ IsSquare a` alone.
-example {a : K} [Fact (¬ IsSquare a)] : Field (QuadraticAlgebra K a 0) := inferInstance
-
 -- The general bridge makes the `Field` instance inferable from `¬ IsSquare (discr a b)`
 -- if `2 ≠ 0` in the field.
 example {a b : ℚ} [Fact (¬ IsSquare (discr a b))] : Field (QuadraticAlgebra ℚ a b) := inferInstance

From b73f458377acafa604ea93fbc7b5b2eab75f7058 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 13 Aug 2026 13:53:01 +0900
Subject: [PATCH 11/15] 1rst commit

---
 Mathlib.lean                                  |   1 +
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean   |  46 ++++++++
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean   |   6 +
 Mathlib/Algebra/QuadraticAlgebra/Int.lean     | 106 ++++++++++++++++++
 .../RingTheory/Localization/FractionRing.lean |   6 +
 5 files changed, 165 insertions(+)
 create mode 100644 Mathlib/Algebra/QuadraticAlgebra/Int.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 40fa39378124c1..66de3b31ac010c 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1208,6 +1208,7 @@ public import Mathlib.Algebra.Prime.Lemmas
 public import Mathlib.Algebra.QuadraticAlgebra.Basic
 public import Mathlib.Algebra.QuadraticAlgebra.Defs
 public import Mathlib.Algebra.QuadraticAlgebra.Discr
+public import Mathlib.Algebra.QuadraticAlgebra.Int
 public import Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
 public import Mathlib.Algebra.QuadraticDiscriminant
 public import Mathlib.Algebra.Quandle
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index bd535f35467d04..3a838bd293363e 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -24,6 +24,8 @@ Let `R` be a commutative ring. We define:
 * `QuadraticAlgebra.map` and `QuadraticAlgebra.mapEquiv`: the `R`-algebra map, respectively
   isomorphism (when `u` is a unit), induced by the change of generator `ω ↦ u • ω + k`
 
+* `QuadraticAlgebra.algHom`: the `R`-algebra map induced by a base change `R → S`
+
 We prove:
 
 * `QuadraticAlgebra.isUnit_iff_norm_isUnit`:
@@ -431,6 +433,50 @@ def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
 
 end map
 
+section algHom
+
+variable {R S : Type*} (S)
+
+section CommSemiring
+
+variable [CommSemiring R] [CommRing S] [Algebra R S] (a b : R)
+
+/-- The `R`-algebra map between quadratic algebras induced by the base change `R → S`,
+sending `ω` to `ω`. -/
+@[simps!]
+def algHom :
+    QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra S (algebraMap R S a) (algebraMap R S b) :=
+  lift ⟨omega, by ext <;> simp [Algebra.algebraMap_eq_smul_one]⟩
+
+theorem algHom_omega :
+    algHom S a b ω = ω := by
+  ext <;> simp
+
+theorem algHom_injective [FaithfulSMul R S] :
+    Function.Injective (algHom S a b) := by
+  intro _ _ h
+  simp only [QuadraticAlgebra.ext_iff, re_algHom_apply, ← Algebra.algebraMap_eq_smul_one,
+    algebraMap.coe_inj, im_algHom_apply] at h
+  exact QuadraticAlgebra.ext_iff.mpr h
+
+end CommSemiring
+
+section CommRing
+
+variable [CommRing R] [CommRing S] [Algebra R S] (a b : R)
+
+theorem norm_algHom (x : QuadraticAlgebra R a b) :
+    norm (algHom S a b x) = algebraMap R S (norm x) := by
+  simp [norm_def, Algebra.smul_def]
+
+theorem trace_algHom (x : QuadraticAlgebra R a b) :
+    trace (algHom S a b x) = algebraMap R S (trace x) := by
+  simp [trace_def, Algebra.smul_def, map_ofNat]
+
+end CommRing
+
+end algHom
+
 section field
 
 variable [Field K] {a b : K} [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)]
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
index 536b5cb1afccee..13b9eecb977e7b 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
@@ -42,6 +42,12 @@ def discr [CommSemiring R] (a b : R) : R := b ^ 2 + 4 * a
 
 theorem discr_def [CommSemiring R] (a b : R) : discr a b = b ^ 2 + 4 * a := rfl
 
+/-- The discriminant commutes with a base change `R → S`. -/
+@[simp]
+theorem discr_algebraMap {S : Type*} [CommSemiring R] [CommSemiring S] [Algebra R S] (a b : R) :
+    discr (algebraMap R S a) (algebraMap R S b) = algebraMap R S (discr a b) := by
+  simp [discr_def, map_ofNat]
+
 /-- Under the change of generator `ω ↦ u • ω + k` (see `QuadraticAlgebra.map`), the
 discriminant is multiplied by `u ^ 2`. -/
 theorem discr_map [CommRing R] (a b u k : R) :
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Int.lean b/Mathlib/Algebra/QuadraticAlgebra/Int.lean
new file mode 100644
index 00000000000000..be2076f94aaaba
--- /dev/null
+++ b/Mathlib/Algebra/QuadraticAlgebra/Int.lean
@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2026 Xavier Roblot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Xavier Roblot
+-/
+module
+
+public import Mathlib.Algebra.QuadraticAlgebra.Discr
+public import Mathlib.RingTheory.Localization.FractionRing
+public import Mathlib.Data.Rat.Lemmas
+
+/-!
+# The quadratic order `QuadraticAlgebra ℤ a b` and its fraction ring
+
+For `a b : ℤ`, `QuadraticAlgebra ℤ a b` is an order in `QuadraticAlgebra ℚ a b`.
+
+## Main results
+
+* `QuadraticAlgebra ℚ a b` is the localization of `QuadraticAlgebra ℤ a b` at the nonzero
+  integers and its fraction ring.
+* `QuadraticAlgebra.Int.isDomain_iff`: `QuadraticAlgebra ℤ a b` is an integral domain iff
+  `discr a b` is not a square.
+-/
+
+@[expose] public section
+
+namespace QuadraticAlgebra
+
+open Algebra
+
+namespace Int
+
+variable {a b : ℤ}
+
+noncomputable instance : Algebra (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
+  (algHom ℚ a b).toRingHom.toAlgebra
+
+instance : IsScalarTower ℤ (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
+  .of_algHom (algHom ℚ a b)
+
+theorem algebraMap_eq (x : QuadraticAlgebra ℤ a b) :
+    algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x = algHom ℚ a b x := rfl
+
+@[simp]
+theorem algebraMap_re_eq (x : QuadraticAlgebra ℤ a b) :
+    (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x).re = x.re := by
+  simp [algebraMap_eq, re_algHom_apply ℚ]
+
+@[simp]
+theorem algebraMap_im_eq (x : QuadraticAlgebra ℤ a b) :
+    (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x).im = x.im := by
+  simp [algebraMap_eq, im_algHom_apply ℚ]
+
+instance : FaithfulSMul (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
+  (faithfulSMul_iff_algebraMap_injective _ _).mpr <| algHom_injective ℚ _ _
+
+/-- The discriminant commutes with the coercion `ℤ → ℚ`. -/
+theorem discr_intCast :
+    discr (a : ℚ) (b : ℚ) = discr a b := by
+  simpa using discr_algebraMap (S := ℚ) a b
+
+open scoped nonZeroDivisors
+
+theorem exists_nat_smul_mem (z : QuadraticAlgebra ℚ a b) :
+    ∃ n : ℕ, 0 < n ∧ n • z ∈ Set.range (algHom ℚ a b) := by
+  obtain ⟨n, hn, x, y, hx, hy⟩ : ∃ n : ℕ, 0 < n ∧ ∃ x y : ℤ, n * z.re = x ∧ n * z.im = y :=
+    ⟨z.re.den * z.im.den, by positivity, z.im.den * z.re.num, z.re.den * z.im.num,
+      by push_cast; grind [← Rat.mul_den_eq_num]⟩
+  refine ⟨n, hn, x • 1 + y • ω, ?_⟩
+  ext <;> simp [re_algHom_apply ℚ, im_algHom_apply ℚ, hx, hy]
+
+/-- `QuadraticAlgebra ℚ a b` is the localization of the order `QuadraticAlgebra ℤ a b` at the
+nonzero integers. This is not `IsFractionRing` in general: `QuadraticAlgebra ℤ a b` need not be a
+domain (see `isDomain_iff`). -/
+noncomputable instance :
+    IsLocalization (algebraMapSubmonoid (QuadraticAlgebra ℤ a b) ℤ⁰)
+      (QuadraticAlgebra ℚ a b) := by
+  refine ⟨fun ⟨y, ⟨x, hx, hy⟩⟩ ↦ ?_, fun x ↦ ?_, fun h ↦ ⟨1, by simpa using h⟩⟩
+  · dsimp only
+    rw [← hy, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply ℤ ℚ]
+    exact IsUnit.map _ <| by simpa [isUnit_iff_ne_zero] using hx
+  · obtain ⟨n, hn, ⟨w, hw⟩⟩ := exists_nat_smul_mem x
+    exact ⟨⟨w, n, ⟨n, by simpa using hn.ne', rfl⟩⟩, by simp [algebraMap_eq, hw, mul_comm]⟩
+
+instance : IsFractionRing (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) := by
+  refine IsLocalization.of_le (algebraMapSubmonoid (QuadraticAlgebra ℤ a b) ℤ⁰) _ ?_ ?_
+  · rintro _ ⟨x, hx, rfl⟩
+    exact norm_mem_nonZeroDivisors_iff.mp <| by simpa using hx
+  · intro x hx
+    rwa [isUnit_iff_norm_isUnit, isUnit_iff_ne_zero, algebraMap_eq, norm_algHom ℚ a b, eq_intCast,
+      Int.cast_ne_zero, ← mem_nonZeroDivisors_iff_ne_zero, norm_mem_nonZeroDivisors_iff]
+
+instance [h : Fact (¬ IsSquare (discr a b))] : Fact (¬ IsSquare (discr (a : ℚ) (b : ℚ))) := by
+  rwa [discr_intCast, Rat.isSquare_intCast_iff]
+
+instance [Fact (¬ IsSquare (discr a b))] : IsDomain (QuadraticAlgebra ℤ a b) :=
+  .of_faithfulSMul _ (QuadraticAlgebra ℚ a b)
+
+theorem isDomain_iff :
+    IsDomain (QuadraticAlgebra ℤ a b) ↔ ¬ IsSquare (discr a b) := by
+  simp [IsFractionRing.isDomain_iff_isField (K := QuadraticAlgebra ℚ a b),
+    isField_iff_not_isSquare_discr, discr_intCast]
+
+end Int
+
+end QuadraticAlgebra
diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean
index 5b194d646d6aca..35594f62ca515a 100644
--- a/Mathlib/RingTheory/Localization/FractionRing.lean
+++ b/Mathlib/RingTheory/Localization/FractionRing.lean
@@ -242,6 +242,12 @@ lemma surjective_iff_isField [IsDomain R] : Function.Surjective (algebraMap R K)
     (IsLocalization.atUnits R _ (S := K)
       (fun _ hx ↦ Ne.isUnit (mem_nonZeroDivisors_iff_ne_zero.mp hx))).surjective
 
+/-- The fraction ring `K` of `R` is a field iff `R` is an integral domain. -/
+theorem isDomain_iff_isField : IsDomain R ↔ IsField K := by
+  refine ⟨fun h ↦ (IsFractionRing.toField R).toIsField K, fun h ↦ ?_⟩
+  let := h.toField
+  exact IsDomain.of_faithfulSMul _ K
+
 end CommRing
 
 variable {B : Type*} [CommRing B] [IsDomain B] [Field K] {L : Type*} [Field L] [Algebra A K]

From c2de8d3aa166d6059961acd1ef9201f3dc7c1d84 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 13 Aug 2026 14:59:35 +0900
Subject: [PATCH 12/15] title

---
 Mathlib/Algebra/QuadraticAlgebra/Int.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Int.lean b/Mathlib/Algebra/QuadraticAlgebra/Int.lean
index be2076f94aaaba..52a3abeba25972 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Int.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Int.lean
@@ -10,7 +10,7 @@ public import Mathlib.RingTheory.Localization.FractionRing
 public import Mathlib.Data.Rat.Lemmas
 
 /-!
-# The quadratic order `QuadraticAlgebra ℤ a b` and its fraction ring
+# Quadratic algebras over `ℤ`
 
 For `a b : ℤ`, `QuadraticAlgebra ℤ a b` is an order in `QuadraticAlgebra ℚ a b`.
 

From 75b8e44e72b32ebadd16cc87fc208129abda8fe6 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Fri, 14 Aug 2026 08:33:03 +0900
Subject: [PATCH 13/15] 1rst commit

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 45 ++++++++++++---------
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean | 10 +++--
 2 files changed, 33 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index d4b1be4ee79d9b..065ad47af42ad5 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -21,8 +21,9 @@ Let `R` be a commutative ring. We define:
 
 * `QuadraticAlgebra.trace`: the trace, as an `R`-linear map
 
-* `QuadraticAlgebra.map` and `QuadraticAlgebra.mapEquiv`: the `R`-algebra map, respectively
-  isomorphism (when `u` is a unit), induced by the change of generator `ω ↦ u • ω + k`
+* `QuadraticAlgebra.changeGenerator` and `QuadraticAlgebra.changeGeneratorEquiv`: the `R`-algebra
+  map, respectively isomorphism (when `u` is a unit), induced by the change of generator
+  `ω ↦ u • ω + k`
 
 We prove:
 
@@ -380,54 +381,62 @@ theorem sq_eq_trace_smul_sub_norm :
 
 end trace
 
-section map
+section changeGenerator
 
 variable [CommRing R]
 
 -- The quadratic relation satisfied by the new generator `u • ω + k`; this is what makes
--- `map` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of the
--- subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds `map` verbatim.
-private theorem map_relation (a b u k : R) :
+-- `changeGenerator` well defined. Stated with `x * x` rather than `x ^ 2` to match the shape of
+-- the subtype condition of `lift` (`{ u // u * u = a • 1 + b • u }`), so it feeds
+-- `changeGenerator` verbatim.
+private theorem changeGenerator_relation (a b u k : R) :
     (u • ω + algebraMap R (QuadraticAlgebra R a b) k) *
         (u • ω + algebraMap R (QuadraticAlgebra R a b) k) =
       (u ^ 2 * a - u * b * k - k ^ 2) • 1 +
         (u * b + 2 * k) • (u • ω + algebraMap R (QuadraticAlgebra R a b) k) := by
   ext <;> simp <;> ring
 
-/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see `map_omega`. -/
+/-- The `R`-algebra map induced by the change of generator `ω ↦ u • ω + k`, see
+`changeGenerator_omega`. -/
 @[simps!]
-def map (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+def changeGenerator (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
     (hb : b' = u * b + 2 * k) :
     QuadraticAlgebra R a' b' →ₐ[R] QuadraticAlgebra R a b :=
-  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact map_relation a b u k⟩
+  lift ⟨u • ω + algebraMap R _ k, by rw [ha, hb]; exact changeGenerator_relation a b u k⟩
 
 @[simp]
-theorem map_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+theorem changeGenerator_omega (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
     (hb : b' = u * b + 2 * k) :
-    map a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
+    changeGenerator a b u k ha hb ω = u • ω + algebraMap R (QuadraticAlgebra R a b) k := by
   ext <;> simp
 
-theorem map_injective (a b u k : R) {a' b' : R} (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
+theorem changeGenerator_injective (a b u k : R) {a' b' : R}
+    (ha : a' = u ^ 2 * a - u * b * k - k ^ 2)
     (hb : b' = u * b + 2 * k) (hu : IsRegular u) :
-    Function.Injective (map a b u k ha hb) := by
+    Function.Injective (changeGenerator a b u k ha hb) := by
   intro z w h
   have hy : z.im = w.im := hu.right <| by simpa using congr_arg im h
   exact QuadraticAlgebra.ext (by simpa [hy] using congr_arg re h) hy
 
-/-- `map` along a unit `u`, as an isomorphism. -/
+/-- `changeGenerator` along a unit `u`, as an isomorphism. -/
 @[simps! apply symm_apply]
-def mapEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
+def changeGeneratorEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
     (ha : a' = (u : R) ^ 2 * a - (u : R) * b * k - k ^ 2)
     (hb : b' = (u : R) * b + 2 * k) :
     QuadraticAlgebra R a' b' ≃ₐ[R] QuadraticAlgebra R a b where
-  __ := map a b u k ha hb
-  invFun := map a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
+  __ := changeGenerator a b u k ha hb
+  invFun := changeGenerator a' b' (u⁻¹ : Rˣ) (-(u⁻¹ : Rˣ) * k)
     (by grind [sq, mul_assoc, Units.inv_mul_cancel_left])
     (by grind [Units.inv_mul_cancel_left])
   left_inv _ := by ext <;> simp [mul_assoc]
   right_inv _ := by ext <;> simp [mul_assoc]
 
-end map
+@[deprecated (since := "2026-08-14")] alias map := changeGenerator
+@[deprecated (since := "2026-08-14")] alias map_omega := changeGenerator_omega
+@[deprecated (since := "2026-08-14")] alias map_injective := changeGenerator_injective
+@[deprecated (since := "2026-08-14")] alias mapEquiv := changeGeneratorEquiv
+
+end changeGenerator
 
 section field
 
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
index 536b5cb1afccee..ead44154b53126 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Discr.lean
@@ -20,8 +20,8 @@ over a field, a criterion for `QuadraticAlgebra K a b` to be a field.
 
 ## Main results
 
-* `QuadraticAlgebra.discr_map`: the discriminant scales by `u ^ 2` under the change of
-  generator `ω ↦ u • ω + k`.
+* `QuadraticAlgebra.discr_changeGenerator`: the discriminant scales by `u ^ 2` under the change
+  of generator `ω ↦ u • ω + k`.
 * `QuadraticAlgebra.exists_sq_eq_iff_isSquare_discr`: over a ring with `2` invertible,
   `X ^ 2 - b * X - a` has a root iff `discr a b` is a square.
 * `QuadraticAlgebra.isField_iff_not_isSquare_discr`: over a field with `2 ≠ 0`,
@@ -42,12 +42,14 @@ def discr [CommSemiring R] (a b : R) : R := b ^ 2 + 4 * a
 
 theorem discr_def [CommSemiring R] (a b : R) : discr a b = b ^ 2 + 4 * a := rfl
 
-/-- Under the change of generator `ω ↦ u • ω + k` (see `QuadraticAlgebra.map`), the
+/-- Under the change of generator `ω ↦ u • ω + k` (see `QuadraticAlgebra.changeGenerator`), the
 discriminant is multiplied by `u ^ 2`. -/
-theorem discr_map [CommRing R] (a b u k : R) :
+theorem discr_changeGenerator [CommRing R] (a b u k : R) :
     discr (u ^ 2 * a - u * b * k - k ^ 2) (u * b + 2 * k) = u ^ 2 * discr a b := by
   rw [discr_def, discr_def]; ring
 
+@[deprecated (since := "2026-08-14")] alias discr_map := discr_changeGenerator
+
 /-- The discriminant is the square of the different `ω - star ω`. -/
 theorem algebraMap_discr [CommRing R] (a b : R) :
     algebraMap R (QuadraticAlgebra R a b) (discr a b) = (ω - star ω) ^ 2 := by

From 658f1af3aae4dd909830f842b3e01600234cd877 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Sat, 15 Aug 2026 14:17:32 +0900
Subject: [PATCH 14/15] rename algHom to baseChange

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 28 ++++++++++-----------
 Mathlib/Algebra/QuadraticAlgebra/Int.lean   | 20 +++++++--------
 2 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index 726afb9cf78bb0..4c11e2e354a636 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -25,7 +25,7 @@ Let `R` be a commutative ring. We define:
   map, respectively isomorphism (when `u` is a unit), induced by the change of generator
   `ω ↦ u • ω + k`
 
-* `QuadraticAlgebra.algHom`: the `R`-algebra map induced by a base change `R → S`
+* `QuadraticAlgebra.baseChange`: the `R`-algebra map induced by a base change `R → S`
 
 We prove:
 
@@ -440,7 +440,7 @@ def changeGeneratorEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
 
 end changeGenerator
 
-section algHom
+section baseChange
 
 variable {R S : Type*} (S)
 
@@ -451,19 +451,19 @@ variable [CommSemiring R] [CommRing S] [Algebra R S] (a b : R)
 /-- The `R`-algebra map between quadratic algebras induced by the base change `R → S`,
 sending `ω` to `ω`. -/
 @[simps!]
-def algHom :
+def baseChange :
     QuadraticAlgebra R a b →ₐ[R] QuadraticAlgebra S (algebraMap R S a) (algebraMap R S b) :=
   lift ⟨omega, by ext <;> simp [Algebra.algebraMap_eq_smul_one]⟩
 
-theorem algHom_omega :
-    algHom S a b ω = ω := by
+theorem baseChange_omega :
+    baseChange S a b ω = ω := by
   ext <;> simp
 
-theorem algHom_injective [FaithfulSMul R S] :
-    Function.Injective (algHom S a b) := by
+theorem baseChange_injective [FaithfulSMul R S] :
+    Function.Injective (baseChange S a b) := by
   intro _ _ h
-  simp only [QuadraticAlgebra.ext_iff, re_algHom_apply, ← Algebra.algebraMap_eq_smul_one,
-    algebraMap.coe_inj, im_algHom_apply] at h
+  simp only [QuadraticAlgebra.ext_iff, re_baseChange_apply, ← Algebra.algebraMap_eq_smul_one,
+    algebraMap.coe_inj, im_baseChange_apply] at h
   exact QuadraticAlgebra.ext_iff.mpr h
 
 end CommSemiring
@@ -472,17 +472,17 @@ section CommRing
 
 variable [CommRing R] [CommRing S] [Algebra R S] (a b : R)
 
-theorem norm_algHom (x : QuadraticAlgebra R a b) :
-    norm (algHom S a b x) = algebraMap R S (norm x) := by
+theorem norm_baseChange (x : QuadraticAlgebra R a b) :
+    norm (baseChange S a b x) = algebraMap R S (norm x) := by
   simp [norm_def, Algebra.smul_def]
 
-theorem trace_algHom (x : QuadraticAlgebra R a b) :
-    trace (algHom S a b x) = algebraMap R S (trace x) := by
+theorem trace_baseChange (x : QuadraticAlgebra R a b) :
+    trace (baseChange S a b x) = algebraMap R S (trace x) := by
   simp [trace_def, Algebra.smul_def, map_ofNat]
 
 end CommRing
 
-end algHom
+end baseChange
 
 section field
 
diff --git a/Mathlib/Algebra/QuadraticAlgebra/Int.lean b/Mathlib/Algebra/QuadraticAlgebra/Int.lean
index 52a3abeba25972..d155d3208d8798 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Int.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Int.lean
@@ -33,26 +33,26 @@ namespace Int
 variable {a b : ℤ}
 
 noncomputable instance : Algebra (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
-  (algHom ℚ a b).toRingHom.toAlgebra
+  (baseChange ℚ a b).toRingHom.toAlgebra
 
 instance : IsScalarTower ℤ (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
-  .of_algHom (algHom ℚ a b)
+  .of_algHom (baseChange ℚ a b)
 
 theorem algebraMap_eq (x : QuadraticAlgebra ℤ a b) :
-    algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x = algHom ℚ a b x := rfl
+    algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x = baseChange ℚ a b x := rfl
 
 @[simp]
 theorem algebraMap_re_eq (x : QuadraticAlgebra ℤ a b) :
     (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x).re = x.re := by
-  simp [algebraMap_eq, re_algHom_apply ℚ]
+  simp [algebraMap_eq, re_baseChange_apply ℚ]
 
 @[simp]
 theorem algebraMap_im_eq (x : QuadraticAlgebra ℤ a b) :
     (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) x).im = x.im := by
-  simp [algebraMap_eq, im_algHom_apply ℚ]
+  simp [algebraMap_eq, im_baseChange_apply ℚ]
 
 instance : FaithfulSMul (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b) :=
-  (faithfulSMul_iff_algebraMap_injective _ _).mpr <| algHom_injective ℚ _ _
+  (faithfulSMul_iff_algebraMap_injective _ _).mpr <| baseChange_injective ℚ _ _
 
 /-- The discriminant commutes with the coercion `ℤ → ℚ`. -/
 theorem discr_intCast :
@@ -62,12 +62,12 @@ theorem discr_intCast :
 open scoped nonZeroDivisors
 
 theorem exists_nat_smul_mem (z : QuadraticAlgebra ℚ a b) :
-    ∃ n : ℕ, 0 < n ∧ n • z ∈ Set.range (algHom ℚ a b) := by
+    ∃ n : ℕ, 0 < n ∧ n • z ∈ Set.range (baseChange ℚ a b) := by
   obtain ⟨n, hn, x, y, hx, hy⟩ : ∃ n : ℕ, 0 < n ∧ ∃ x y : ℤ, n * z.re = x ∧ n * z.im = y :=
     ⟨z.re.den * z.im.den, by positivity, z.im.den * z.re.num, z.re.den * z.im.num,
       by push_cast; grind [← Rat.mul_den_eq_num]⟩
   refine ⟨n, hn, x • 1 + y • ω, ?_⟩
-  ext <;> simp [re_algHom_apply ℚ, im_algHom_apply ℚ, hx, hy]
+  ext <;> simp [re_baseChange_apply ℚ, im_baseChange_apply ℚ, hx, hy]
 
 /-- `QuadraticAlgebra ℚ a b` is the localization of the order `QuadraticAlgebra ℤ a b` at the
 nonzero integers. This is not `IsFractionRing` in general: `QuadraticAlgebra ℤ a b` need not be a
@@ -87,8 +87,8 @@ instance : IsFractionRing (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b)
   · rintro _ ⟨x, hx, rfl⟩
     exact norm_mem_nonZeroDivisors_iff.mp <| by simpa using hx
   · intro x hx
-    rwa [isUnit_iff_norm_isUnit, isUnit_iff_ne_zero, algebraMap_eq, norm_algHom ℚ a b, eq_intCast,
-      Int.cast_ne_zero, ← mem_nonZeroDivisors_iff_ne_zero, norm_mem_nonZeroDivisors_iff]
+    rwa [isUnit_iff_norm_isUnit, isUnit_iff_ne_zero, algebraMap_eq, norm_baseChange ℚ a b,
+      eq_intCast, Int.cast_ne_zero, ← mem_nonZeroDivisors_iff_ne_zero, norm_mem_nonZeroDivisors_iff]
 
 instance [h : Fact (¬ IsSquare (discr a b))] : Fact (¬ IsSquare (discr (a : ℚ) (b : ℚ))) := by
   rwa [discr_intCast, Rat.isSquare_intCast_iff]

From 091b59aa7f783086a0ef0ecb35172e8bedfd4813 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Fri, 21 Aug 2026 09:03:56 +0200
Subject: [PATCH 15/15] delete instance

---
 Mathlib/Algebra/QuadraticAlgebra/Int.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Int.lean b/Mathlib/Algebra/QuadraticAlgebra/Int.lean
index d155d3208d8798..9649c28b0d2db1 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Int.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Int.lean
@@ -90,12 +90,6 @@ instance : IsFractionRing (QuadraticAlgebra ℤ a b) (QuadraticAlgebra ℚ a b)
     rwa [isUnit_iff_norm_isUnit, isUnit_iff_ne_zero, algebraMap_eq, norm_baseChange ℚ a b,
       eq_intCast, Int.cast_ne_zero, ← mem_nonZeroDivisors_iff_ne_zero, norm_mem_nonZeroDivisors_iff]
 
-instance [h : Fact (¬ IsSquare (discr a b))] : Fact (¬ IsSquare (discr (a : ℚ) (b : ℚ))) := by
-  rwa [discr_intCast, Rat.isSquare_intCast_iff]
-
-instance [Fact (¬ IsSquare (discr a b))] : IsDomain (QuadraticAlgebra ℤ a b) :=
-  .of_faithfulSMul _ (QuadraticAlgebra ℚ a b)
-
 theorem isDomain_iff :
     IsDomain (QuadraticAlgebra ℤ a b) ↔ ¬ IsSquare (discr a b) := by
   simp [IsFractionRing.isDomain_iff_isField (K := QuadraticAlgebra ℚ a b),