From 66b887743821c028c9d89b58d1407872c1006910 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 20 Aug 2026 13:54:26 +0200
Subject: [PATCH 1/2] 1st commit

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 45 +++++++++++++++++++++
 Mathlib/Algebra/QuadraticAlgebra/Discr.lean |  6 +++
 2 files changed, 51 insertions(+)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index 065ad47af42ad5..851f48644ce89b 100644
--- a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
+++ b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
@@ -23,6 +23,7 @@ Let `R` be a commutative ring. We define:
 
 * `QuadraticAlgebra.changeGenerator` and `QuadraticAlgebra.changeGeneratorEquiv`: the `R`-algebra
   map, respectively isomorphism (when `u` is a unit), induced by the change of generator
+* `QuadraticAlgebra.baseChange`: the `R`-algebra map induced by a base change `R → S`
   `ω ↦ u • ω + k`
 
 We prove:
@@ -438,6 +439,50 @@ def changeGeneratorEquiv (a b : R) (u : Rˣ) (k : R) {a' b' : R}
 
 end changeGenerator
 
+section baseChange
+
+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 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 baseChange_omega :
+    baseChange S a b ω = ω := by
+  ext <;> simp
+
+theorem baseChange_injective [FaithfulSMul R S] :
+    Function.Injective (baseChange S a b) := by
+  intro _ _ 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
+
+section CommRing
+
+variable [CommRing R] [CommRing S] [Algebra R S] (a b : R)
+
+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_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 baseChange
+
 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 ead44154b53126..f392a2ec33ef65 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.changeGenerator`), the
 discriminant is multiplied by `u ^ 2`. -/
 theorem discr_changeGenerator [CommRing R] (a b u k : R) :

From d6f3bff3472ff72810cd491e8a9258b278f60fbb Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Thu, 20 Aug 2026 14:03:25 +0200
Subject: [PATCH 2/2] docstring

---
 Mathlib/Algebra/QuadraticAlgebra/Basic.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Algebra/QuadraticAlgebra/Basic.lean b/Mathlib/Algebra/QuadraticAlgebra/Basic.lean
index 851f48644ce89b..2a50cab91aa6df 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, norm, trace, and change of generator.
+# Quadratic algebras: involution, norm, trace, change of generator, etc.
 
 Let `R` be a commutative ring. We define:
 
@@ -23,9 +23,10 @@ Let `R` be a commutative ring. We define:
 
 * `QuadraticAlgebra.changeGenerator` and `QuadraticAlgebra.changeGeneratorEquiv`: the `R`-algebra
   map, respectively isomorphism (when `u` is a unit), induced by the change of generator
-* `QuadraticAlgebra.baseChange`: the `R`-algebra map induced by a base change `R → S`
   `ω ↦ u • ω + k`
 
+* `QuadraticAlgebra.baseChange`: the `R`-algebra homomorphism induced by a base change `R → S`
+
 We prove:
 
 * `QuadraticAlgebra.isUnit_iff_norm_isUnit`: