Basic results about modules over the rationals.

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

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

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

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

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.

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.

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.

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.

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

instance IsScalarTower.rat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module ℚ R] [Module ℚ M] : IsScalarTower ℚ R M

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.

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.

instance SMulCommClass.nnrat {α : Type u} {M : Type v} [AddCommMonoid M] [DistribSMul α M] [Module ℚ≥0 M] : SMulCommClass ℚ≥0 α M

instance SMulCommClass.rat {α : Type u} {M : Type v} [AddCommGroup M] [DistribSMul α M] [Module ℚ M] : SMulCommClass ℚ α M

instance SMulCommClass.nnrat' {α : Type u} {M : Type v} [AddCommMonoid M] [DistribSMul α M] [Module ℚ≥0 M] : SMulCommClass α ℚ≥0 M

instance SMulCommClass.rat' {α : Type u} {M : Type v} [AddCommGroup M] [DistribSMul α M] [Module ℚ M] : SMulCommClass α ℚ M

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.

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.