Feat/2 quadratic param uniqueness

Mathlib.lean

@@ -5585,6 +5585,7 @@ public import Mathlib.NumberTheory.PrimeCounting
 public import Mathlib.NumberTheory.PrimesCongruentOne
 public import Mathlib.NumberTheory.Primorial
 public import Mathlib.NumberTheory.PythagoreanTriples
+public import Mathlib.NumberTheory.QuadraticField.Basic
 public import Mathlib.NumberTheory.RamificationInertia.Basic
 public import Mathlib.NumberTheory.RamificationInertia.Galois
 public import Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Mathlib/Algebra/QuadraticAlgebra/Defs.lean

@@ -7,6 +7,8 @@ module
 
 public import Mathlib.LinearAlgebra.Dimension.StrongRankCondition
 public import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
+public import Mathlib.LinearAlgebra.Matrix.Notation
+public import Mathlib.LinearAlgebra.Matrix.ToLin
 
 
 /-!
@@ -461,6 +463,16 @@ instance [CommSemiring S] [Algebra S R] : Algebra S (QuadraticAlgebra R a b) whe
   commutes' s z := by ext <;> simp [Algebra.commutes]
   smul_def' s x := by ext <;> simp [Algebra.smul_def]
 
+/-- The left multiplication matrix of an element in `QuadraticAlgebra R a b`
+with respect to the basis `{1, i}`. -/
+theorem leftMulMatrix_eq (x : QuadraticAlgebra R a b) :
+    Algebra.leftMulMatrix (basis a b) x = !![x.re, a * x.im; x.im, x.re + b * x.im] := by
+  ext i j
+  fin_cases i <;> fin_cases j
+  all_goals
+    rw [Algebra.leftMulMatrix_apply, LinearMap.toMatrix_apply]
+    simp [QuadraticAlgebra.basis]
+
 theorem algebraMap_eq (r : R) : algebraMap R (QuadraticAlgebra R a b) r = ⟨r, 0⟩ := rfl
 
 theorem algebraMap_injective : (algebraMap R (QuadraticAlgebra R a b) : _ → _).Injective :=

Mathlib/Algebra/Squarefree/Basic.lean

@@ -83,6 +83,22 @@ theorem Squarefree.of_mul_right [CommMonoid R] {m n : R} (hmn : Squarefree (m *
 theorem Squarefree.squarefree_of_dvd [Monoid R] {x y : R} (hdvd : x ∣ y) (hsq : Squarefree y) :
     Squarefree x := fun _ h => hsq _ (h.trans hdvd)
 
+/-- If `a * a` is squarefree, then `a` is a unit. -/
+theorem Squarefree.isUnit_of_mul_self [Monoid R] {a : R}
+    (h : Squarefree (a * a)) : IsUnit a :=
+  h a ⟨1, (mul_one _).symm⟩
+
+/-- A squarefree element that is a perfect square must be a unit. -/
+theorem Squarefree.isUnit_of_isSquare [Monoid R] {a : R}
+    (hsf : Squarefree a) (hsq : IsSquare a) : IsUnit a := by
+  obtain ⟨z, rfl⟩ := hsq
+  simp [hsf.isUnit_of_mul_self]
+
+/-- A squarefree non-unit element is not a perfect square. -/
+theorem Squarefree.not_isSquare [Monoid R] {a : R}
+    (hsf : Squarefree a) (ha : ¬ IsUnit a) : ¬ IsSquare a :=
+  fun hsq ↦ ha (hsf.isUnit_of_isSquare hsq)
+
 theorem Associated.squarefree_iff [Monoid R] {x y : R} (h : Associated x y) :
     Squarefree x ↔ Squarefree y :=
   ⟨fun hx ↦ hx.squarefree_of_dvd h.dvd', fun hy ↦ hy.squarefree_of_dvd h.dvd⟩