Documentation

Mathlib.Algebra.Algebra.Rat

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.

Equations
Equations
  • =
instance NNRat.instSMulCommClass {R : Type u_2} {S : Type u_3} [DivisionSemiring S] [CharZero S] [SMul R S] [SMulCommClass R S S] :
Equations
  • =
instance NNRat.instSMulCommClass' {R : Type u_2} {S : Type u_3} [DivisionSemiring S] [CharZero S] [SMul R S] [SMulCommClass S R S] :
Equations
  • =
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.

Equations
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] :
Equations
  • =
instance Rat.instSMulCommClass {R : Type u_2} {S : Type u_3} [DivisionRing S] [CharZero S] [SMul R S] [SMulCommClass R S S] :
Equations
  • =
instance Rat.instSMulCommClass' {R : Type u_2} {S : Type u_3} [DivisionRing S] [CharZero S] [SMul R S] [SMulCommClass S R S] :
Equations
  • =
@[deprecated Algebra.id.map_eq_id]
Equations
  • =