# Basic results about modules over the rationals. #

source
theorem map_nnratCast_smul {M : Type u_1} {M₂ : Type u_2} [AddCommMonoid M] [AddCommMonoid M₂] {F : Type u_3} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5) [DivisionSemiring R] [DivisionSemiring S] [Module R M] [Module S M₂] (c : ℚ≥0) (x : M) :
f (↑c • x) = ↑c • f x
source
theorem map_ratCast_smul {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_3} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_4) (S : Type u_5) [DivisionRing R] [DivisionRing S] [Module R M] [Module S M₂] (c : ℚ) (x : M) :
f (↑c • x) = ↑c • f x
source
theorem map_nnrat_smul {M : Type u_1} {M₂ : Type u_2} [AddCommMonoid M] [AddCommMonoid M₂] [_instM : Module ℚ≥0 M] [_instM₂ : Module ℚ≥0 M₂] {F : Type u_3} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (c : ℚ≥0) (x : M) :
f (c • x) = c • f x
source
theorem map_rat_smul {M : Type u_1} {M₂ : Type u_2} [AddCommGroup M] [AddCommGroup M₂] [_instM : Module ℚ M] [_instM₂ : Module ℚ M₂] {F : Type u_3} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (c : ℚ) (x : M) :
f (c • x) = c • f x
source
instance subsingleton_nnrat_module (E : Type u_3) [AddCommMonoid E] :
Subsingleton (Module ℚ≥0 E)

There can be at most one `Module ℚ≥0 E` structure on an additive commutative monoid.

source
instance subsingleton_rat_module (E : Type u_3) [AddCommGroup E] :
Subsingleton (Module ℚ E)

There can be at most one `Module ℚ E` structure on an additive commutative group.

source
theorem nnratCast_smul_eq {E : Type u_3} (R : Type u_4) (S : Type u_5) [AddCommMonoid E] [DivisionSemiring R] [DivisionSemiring S] [Module R E] [Module S E] (r : ℚ≥0) (x : E) :
↑r • x = ↑r • x

If `E` is a vector space over two division semirings `R` and `S`, then scalar multiplications agree on non-negative rational numbers in `R` and `S`.

source
theorem ratCast_smul_eq {E : Type u_3} (R : Type u_4) (S : Type u_5) [AddCommGroup E] [DivisionRing R] [DivisionRing S] [Module R E] [Module S E] (r : ℚ) (x : E) :
↑r • x = ↑r • x

If `E` is a vector space over two division rings `R` and `S`, then scalar multiplications agree on rational numbers in `R` and `S`.

source
instance IsScalarTower.nnrat {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module ℚ≥0 R] [Module ℚ≥0 M] :
IsScalarTower ℚ≥0 R M
source
instance IsScalarTower.rat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module ℚ R] [Module ℚ M] :
IsScalarTower ℚ R M
source
theorem NNRat.cast_smul_eq_nnqsmul {M : Type u_1} (R : Type u_3) [DivisionSemiring R] [MulAction R M] [MulAction ℚ≥0 M] [IsScalarTower ℚ≥0 R M] (q : ℚ≥0) (x : M) :
↑q • x = q • x

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

source
theorem Rat.cast_smul_eq_qsmul {M : Type u_1} (R : Type u_3) [DivisionRing R] [MulAction R M] [MulAction ℚ M] [IsScalarTower ℚ R M] (q : ℚ) (x : M) :
↑q • x = q • x

`qsmul` is equal to any other module structure via a cast.

source
instance SMulCommClass.nnrat {α : Type u} {M : Type v} [Monoid α] [AddCommMonoid M] [DistribMulAction α M] [Module ℚ≥0 M] :
SMulCommClass ℚ≥0 α M
source
instance SMulCommClass.rat {α : Type u} {M : Type v} [Monoid α] [AddCommGroup M] [DistribMulAction α M] [Module ℚ M] :
SMulCommClass ℚ α M
source
instance SMulCommClass.nnrat' {α : Type u} {M : Type v} [Monoid α] [AddCommMonoid M] [DistribMulAction α M] [Module ℚ≥0 M] :
SMulCommClass α ℚ≥0 M
source
instance SMulCommClass.rat' {α : Type u} {M : Type v} [Monoid α] [AddCommGroup M] [DistribMulAction α M] [Module ℚ M] :
SMulCommClass α ℚ M
source
theorem IsAddTorsionFree.of_module_nnrat (M : Type u_1) [AddCommMonoid M] [Module ℚ≥0 M] :
IsAddTorsionFree M

A `ℚ≥0`-module is torsion-free as a group.

This instance will fire for any monoid `M`, so is local unless needed elsewhere.

source
theorem IsAddTorsionFree.of_module_rat (M : Type u_1) [AddCommGroup M] [Module ℚ M] :
IsAddTorsionFree M

A `ℚ≥0`-module is torsion-free as a group.

This instance will fire for any monoid `M`, so is local unless needed elsewhere.