instance QuadraticAlgebra.instAlgebraCoeRingHomAlgebraMap_formalConjecturesForMathlib {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommRing S] [Algebra R S] (a b : R) : Algebra (QuadraticAlgebra R a b) (QuadraticAlgebra S ((algebraMap R S) a) ((algebraMap R S) b))

Equations

• QuadraticAlgebra.instAlgebraCoeRingHomAlgebraMap_formalConjecturesForMathlib a b = (QuadraticAlgebra.lift ⟨QuadraticAlgebra.omega, ⋯⟩).toAlgebra

@[simp]

theorem QuadraticAlgebra.algebraMap_omega {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommRing S] [Algebra R S] (a b : R) : (algebraMap (QuadraticAlgebra R a b) (QuadraticAlgebra S ((algebraMap R S) a) ((algebraMap R S) b))) omega = omega

instance QuadraticAlgebra.instAlgebraIntCast_formalConjecturesForMathlib {S : Type u_2} [CommRing S] (a b : ℤ) : Algebra (QuadraticAlgebra ℤ a b) (QuadraticAlgebra S ↑a ↑b)

Equations

• QuadraticAlgebra.instAlgebraIntCast_formalConjecturesForMathlib a b = (QuadraticAlgebra.lift ⟨QuadraticAlgebra.omega, ⋯⟩).toAlgebra

@[simp]

theorem QuadraticAlgebra.algebraMap_omega' {S : Type u_2} [CommRing S] (a b : ℤ) : (algebraMap (QuadraticAlgebra ℤ a b) (QuadraticAlgebra S ↑a ↑b)) omega = omega

instance QuadraticAlgebra.instAlgebraIntOfNatCast_formalConjecturesForMathlib {S : Type u_2} [CommRing S] (a : ℤ) : Algebra (QuadraticAlgebra ℤ a 0) (QuadraticAlgebra S (↑a) 0)

Equations

• QuadraticAlgebra.instAlgebraIntOfNatCast_formalConjecturesForMathlib a = (QuadraticAlgebra.lift ⟨QuadraticAlgebra.omega, ⋯⟩).toAlgebra

@[simp]

theorem QuadraticAlgebra.algebraMap_omega'' {S : Type u_2} [CommRing S] (a : ℤ) : (algebraMap (QuadraticAlgebra ℤ a 0) (QuadraticAlgebra S (↑a) 0)) omega = omega

instance QuadraticAlgebra.fact_field {d : ℤ} [Fact (Squarefree d)] [Fact (d ≠ 1)] : Fact (∀ (r : ℚ), r ^ 2 ≠ ↑d + 0 * r)