Documentation

Mathlib.Algebra.Module.Rat

Basic results about modules over the rationals. #

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
@[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.

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_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
  • ⋯ = ⋯
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
@[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.

source
instance IsScalarTower.rat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module ℚ R] [Module ℚ M] :
IsScalarTower ℚ R M
Equations
  • ⋯ = ⋯
source
instance SMulCommClass.rat {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] :
SMulCommClass ℚ R M
Equations
  • ⋯ = ⋯
source
instance SMulCommClass.rat' {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] :
SMulCommClass R ℚ M
Equations
  • ⋯ = ⋯
source
@[instance 100]
instance RatModule.noZeroSMulDivisors {M : Type u_1} [AddCommGroup M] [Module ℚ M] :
NoZeroSMulDivisors ℤ M
Equations
  • ⋯ = ⋯