/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.Algebra.QuadraticAlgebra.Basic public import Mathlib.Algebra.Squarefree.Basicpublic sectionnamespace QuadraticAlgebravariable {R S : Type*} [CommSemiring R] [CommRing S] [Algebra R S]instance (a b : R) : Algebra (QuadraticAlgebra R a b) (QuadraticAlgebra S (algebraMap R S a) (algebraMap R S b)) := (lift ⟨ω, byR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommRing Sinst✝:Algebra R Sa:Rb:R⊢ ω * ω = a • 1 + b • ω simpa using omega_mul_omega_eq_add (a := algebraMap R S a) (b := algebraMap R S b)All goals completed! 🐙⟩).toRingHom.toAlgebra@[simp] lemma algebraMap_omega (a b : R) : algebraMap (QuadraticAlgebra R a b) (QuadraticAlgebra S (algebraMap R S a) (algebraMap R S b)) ω = ω := byR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommRing Sinst✝:Algebra R Sa:Rb:R⊢ (algebraMap (QuadraticAlgebra R a b) (QuadraticAlgebra S ((algebraMap R S) a) ((algebraMap R S) b))) ω = ω convert! lift_symm_apply_coe _e'_3R:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommRing Sinst✝:Algebra R Sa:Rb:R⊢ ω = (lift ⟨ω, ⋯⟩) ω simpAll goals completed! 🐙instance (a b : ℤ) : Algebra (QuadraticAlgebra ℤ a b) (QuadraticAlgebra S a b) := (lift ⟨ω, byR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommRing Sinst✝:Algebra R Sa:ℤb:ℤ⊢ ω * ω = a • 1 + b • ω simpa [Int.cast_smul_eq_zsmul] using omega_mul_omega_eq_add (R := S) (a := a) (b := b)All goals completed! 🐙⟩).toRingHom.toAlgebra@[simp] lemma algebraMap_omega' (a b : ℤ) : algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra S a b) ω = ω := byS:Type u_2inst✝:CommRing Sa:ℤb:ℤ⊢ (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra S ↑a ↑b)) ω = ω simpa using algebraMap_omega (S := S) a bAll goals completed! 🐙instance (a : ℤ) : Algebra (QuadraticAlgebra ℤ a 0) (QuadraticAlgebra S a 0) := (lift ⟨ω, byR:Type u_1S:Type u_2inst✝²:CommSemiring Rinst✝¹:CommRing Sinst✝:Algebra R Sa:ℤ⊢ ω * ω = a • 1 + 0 • ω simpa [Int.cast_smul_eq_zsmul] using omega_mul_omega_eq_add (R := S) (a := a) (b := 0)All goals completed! 🐙⟩).toRingHom.toAlgebra@[simp] lemma algebraMap_omega'' (a : ℤ) : algebraMap (QuadraticAlgebra ℤ a 0) (QuadraticAlgebra S a 0) ω = ω := byS:Type u_2inst✝:CommRing Sa:ℤ⊢ (algebraMap (QuadraticAlgebra ℤ a 0) (QuadraticAlgebra S (↑a) 0)) ω = ω convert! lift_symm_apply_coe _e'_3S:Type u_2inst✝:CommRing Sa:ℤ⊢ ω = (lift ⟨ω, ⋯⟩) ω simpAll goals completed! 🐙variable {d : ℤ} [Fact <| Squarefree d] [Fact <| d ≠ 1] instance fact_field : Fact (∀ r : ℚ, r ^ 2 ≠ d + 0 * r) := byR:Type u_1S:Type u_2inst✝⁴:CommSemiring Rinst✝³:CommRing Sinst✝²:Algebra R Sd:ℤinst✝¹:Fact (Squarefree d)inst✝:Fact (d ≠ 1)⊢ Fact (∀ (r : ℚ), r ^ 2 ≠ ↑d + 0 * r) refine ⟨fun r h ↦ ?_⟩R:Type u_1S:Type u_2inst✝⁴:CommSemiring Rinst✝³:CommRing Sinst✝²:Algebra R Sd:ℤinst✝¹:Fact (Squarefree d)inst✝:Fact (d ≠ 1)r:ℚh:r ^ 2 = ↑d + 0 * r⊢ False obtain ⟨s, hs⟩ : IsSquare d := Rat.isSquare_intCast_iff.1 ⟨r, byR:Type u_1S:Type u_2inst✝⁴:CommSemiring Rinst✝³:CommRing Sinst✝²:Algebra R Sd:ℤinst✝¹:Fact (Squarefree d)inst✝:Fact (d ≠ 1)r:ℚh:r ^ 2 = ↑d + 0 * r⊢ ↑d = r * rR:Type u_1S:Type u_2inst✝⁴:CommSemiring Rinst✝³:CommRing Sinst✝²:Algebra R Sd:ℤinst✝¹:Fact (Squarefree d)inst✝:Fact (d ≠ 1)r:ℚh:r ^ 2 = ↑d + 0 * rs:ℤhs:d = s * s⊢ False grindAll goals completed! 🐙R:Type u_1S:Type u_2inst✝⁴:CommSemiring Rinst✝³:CommRing Sinst✝²:Algebra R Sd:ℤinst✝¹:Fact (Squarefree d)inst✝:Fact (d ≠ 1)r:ℚh:r ^ 2 = ↑d + 0 * rs:ℤhs:d = s * s⊢ False⟩R:Type u_1S:Type u_2inst✝⁴:CommSemiring Rinst✝³:CommRing Sinst✝²:Algebra R Sd:ℤinst✝¹:Fact (Squarefree d)inst✝:Fact (d ≠ 1)r:ℚh:r ^ 2 = ↑d + 0 * rs:ℤhs:d = s * s⊢ False grind [Int.isUnit_mul_self <| (Fact.out : Squarefree d) s hs.symm.dvd, (Fact.out : d ≠ 1)]All goals completed! 🐙end QuadraticAlgebra