instance QuadraticAlgebra.instAlgebraCoeRingHomAlgebraMap {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 a b = (QuadraticAlgebra.lift ⟨QuadraticAlgebra.omega, ⋯⟩).toAlgebra

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

Equations

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

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

Equations

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