Further basic results about Algebra's over ℚ.

This file could usefully be split further.

@[simp]

theorem RingHom.map_rat_algebraMap {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] [Algebra ℚ R] [Algebra ℚ S] (f : R →+* S) (r : ℚ) : f ((algebraMap ℚ R) r) = (algebraMap ℚ S) r

theorem NNRat.cast_smul_eq_nnqsmul (R : Type u_2) {S : Type u_3} [DivisionSemiring R] [CharZero R] [Semiring S] [Module ℚ≥0 S] [Module R S] (q : ℚ≥0) (a : S) : ↑q • a = q • a

nnqsmul is equal to any other module structure via a cast.

instance DivisionSemiring.toNNRatAlgebra {R : Type u_2} [DivisionSemiring R] [CharZero R] : Algebra ℚ≥0 R

Equations

• DivisionSemiring.toNNRatAlgebra = Algebra.mk (NNRat.castHom R) ⋯ ⋯

instance RingHomClass.toLinearMapClassNNRat {F : Type u_1} {R : Type u_2} {S : Type u_3} [DivisionSemiring R] [CharZero R] [DivisionSemiring S] [CharZero S] [FunLike F R S] [RingHomClass F R S] : LinearMapClass F ℚ≥0 R S

instance NNRat.instSMulCommClass {R : Type u_2} {S : Type u_3} [DivisionSemiring S] [CharZero S] [SMul R S] [SMulCommClass R S S] : SMulCommClass ℚ≥0 R S

instance NNRat.instSMulCommClass' {R : Type u_2} {S : Type u_3} [DivisionSemiring S] [CharZero S] [SMul R S] [SMulCommClass S R S] : SMulCommClass R ℚ≥0 S

theorem Rat.cast_smul_eq_qsmul (R : Type u_2) {S : Type u_3} [DivisionRing R] [CharZero R] [Ring S] [Module ℚ S] [Module R S] (q : ℚ) (a : S) : ↑q • a = q • a

nnqsmul is equal to any other module structure via a cast.

instance DivisionRing.toRatAlgebra {R : Type u_2} [DivisionRing R] [CharZero R] : Algebra ℚ R

Equations

• DivisionRing.toRatAlgebra = Algebra.mk (Rat.castHom R) ⋯ ⋯

instance RingHomClass.toLinearMapClassRat {F : Type u_1} {R : Type u_2} {S : Type u_3} [DivisionRing R] [CharZero R] [DivisionRing S] [CharZero S] [FunLike F R S] [RingHomClass F R S] : LinearMapClass F ℚ R S

instance Rat.instSMulCommClass {R : Type u_2} {S : Type u_3} [DivisionRing S] [CharZero S] [SMul R S] [SMulCommClass R S S] : SMulCommClass ℚ R S

instance Rat.instSMulCommClass' {R : Type u_2} {S : Type u_3} [DivisionRing S] [CharZero S] [SMul R S] [SMulCommClass S R S] : SMulCommClass R ℚ S

@[deprecated Algebra.id.map_eq_id (since := "2024-07-30")]

theorem algebraMap_rat_rat : algebraMap ℚ ℚ = RingHom.id ℚ

instance Rat.algebra_rat_subsingleton {R : Type u_4} [Semiring R] : Subsingleton (Algebra ℚ R)