refactor(Algebra/QuadraticAlgebra): crush ℚ-algebra diamond (#38818)

From FormalConjectures

Author: YaelDillies

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

@@ -8,15 +8,18 @@ module
 public import Mathlib.Algebra.QuadraticAlgebra.Defs
 public import Mathlib.Algebra.Star.Unitary
 
-/-! # Quadratic algebras : involution and norm.
+import Mathlib.Tactic.FieldSimp
+
+/-!
+# Quadratic algebras: involution and norm.
 
 Let `R` be a commutative ring. We define:
 
-* `QuadraticAlgebra.star` : the quadratic involution
+* `QuadraticAlgebra.star`: the quadratic involution
 
-* `QuadraticAlgebra.norm` : the norm
+* `QuadraticAlgebra.norm`: the norm
 
-We prove :
+We prove:
 
 * `QuadraticAlgebra.isUnit_iff_norm_isUnit`:
   `w : QuadraticAlgebra R a b` is a unit iff `w.norm` is a unit in `R`.
@@ -25,19 +28,14 @@ We prove :
   `w : QuadraticAlgebra R a b` isn't a zero divisor iff
   `w.norm` isn't a zero divisor in `R`.
 
-* If `R` is a field, and `∀ r, r ^ 2 ≠ a + b * r`, then `QuadraticAlgebra R a b` is a field.
-
-## Warning
-If you are working over `ℚ`, note the existence of the diamond explained in
-`Mathlib.Algebra.QuadraticAlgebra.Defs`.
-
+* If `K` is a field, and `∀ r, r ^ 2 ≠ a + b * r`, then `QuadraticAlgebra K a b` is a field.
 -/
 
 @[expose] public section
 
 namespace QuadraticAlgebra
 
-variable {R : Type*} {a b : R}
+variable {K R : Type*} {a b : R}
 
 section omega
 
@@ -313,9 +311,9 @@ end norm
 
 section field
 
-variable [Field R] [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)]
+variable [Field K] {a b : K} [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)]
 
-lemma norm_eq_zero_iff_eq_zero {z : QuadraticAlgebra R a b} :
+lemma norm_eq_zero_iff_eq_zero {z : QuadraticAlgebra K a b} :
     norm z = 0 ↔ z = 0 := by
   constructor
   · intro hz
@@ -330,20 +328,27 @@ lemma norm_eq_zero_iff_eq_zero {z : QuadraticAlgebra R a b} :
   · intro hz
     simp [hz]
 
-/-- If `R` is a field and there is no `r : R` such that `r ^ 2 = a + b * r`,
-then `QuadraticAlgebra R a b` is a field. -/
-instance : Field (QuadraticAlgebra R a b) where
-  inv z := (norm z)⁻¹ • star z
+@[simps] instance : NNRatCast (QuadraticAlgebra K a b) where nnratCast q := ⟨q, 0⟩
+@[simps] instance : RatCast (QuadraticAlgebra K a b) where ratCast q := ⟨q, 0⟩
+
+@[simps -isSimp, simps!] instance : Inv (QuadraticAlgebra K a b) where inv z := (norm z)⁻¹ • star z
+@[simps -isSimp, simps!] instance : Div (QuadraticAlgebra K a b) where div w z := w * z⁻¹
+
+/-- If `K` is a field and there is no `r : K` such that `r ^ 2 = a + b * r`,
+then `QuadraticAlgebra K a b` is a field. -/
+instance : Field (QuadraticAlgebra K a b) where
+  inv_zero := by ext <;> simp
   mul_inv_cancel z hz := by
     rw [ne_eq, ← norm_eq_zero_iff_eq_zero] at hz
-    simp only [Algebra.mul_smul_comm]
+    simp only [inv_def, Algebra.mul_smul_comm]
     rw [← C_mul_eq_smul, C_eq_algebraMap, ← algebraMap_norm_eq_mul_star, ← map_mul,
       inv_mul_cancel₀ hz, map_one]
-  inv_zero := by simp
-  nnqsmul := _
-  nnqsmul_def := fun _ _ => rfl
-  qsmul := _
-  qsmul_def := fun _ _ => rfl
+  nnratCast_def q := by ext <;> simp [sq]; field_simp; simp [NNRat.cast_def]
+  ratCast_def q := by ext <;> simp [sq]; field_simp; simp [Rat.cast_def]
+  nnqsmul := (· • ·)
+  qsmul := (· • ·)
+  nnqsmul_def q x := by ext <;> simp [NNRat.smul_def]
+  qsmul_def q x := by ext <;> simp [Rat.smul_def]
 
 end field
 

Mathlib/Algebra/QuadraticAlgebra/Defs.lean

@@ -21,20 +21,6 @@ and define some algebraic structures on it.
 * `QuadraticAlgebra R a b`:
   [Bourbaki, *Algebra I*][bourbaki1989] with coefficients `a`, `b` in `R`.
 
-## Warning
-If `R` is a ring, then `QuadraticAlgebra a b` is an `R`-algebra, and if `R` is of characteristic
-zero then the same holds for `QuadraticAlgebra a b`. In particular, in the very common case where
-`R` is `ℚ` and `a` and `b` are such that `QuadraticAlgebra a b` is a field, then
-`QuadraticAlgebra a b` is a `ℚ`-algebra in two ways, that are not definitionally equal. This is a
-known diamond for characteristic zero fields. If you are working in this setting you should start
-your file with
-```
-attribute [-instance] DivisionRing.toRatAlgebra
-```
-to keep the `CharZero` instance but to avoid having two `Algebra` instances. (Note that all the
-basic theorems about `QuadraticAlgebra` are stated using the general instance
-`Algebra R (QuadraticAlgebra a b)`, so you don't want to deactivate that one.)
-
 ## Tags
 
 Quadratic algebra, quadratic extension