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

@[deprecated map_ratCast_smul]

theorem map_rat_cast_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

Alias of map_ratCast_smul.

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.

Equations

• ⋯ = ⋯

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.

Equations

• ⋯ = ⋯

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.

@[deprecated ratCast_smul_eq]

theorem rat_cast_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

Alias of ratCast_smul_eq.

---

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 100]

instance NNRatModule.noZeroSMulDivisors {M : Type u_1} [AddCommMonoid M] [Module ℚ≥0 M] : NoZeroSMulDivisors ℕ M

Equations

• ⋯ = ⋯

@[instance 100]

instance RatModule.noZeroSMulDivisors {M : Type u_1} [AddCommGroup M] [Module ℚ M] : NoZeroSMulDivisors ℤ M

Equations

• ⋯ = ⋯