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)
:
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)
:
@[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)
:
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)
:
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)
:
There can be at most one Module ℚ≥0 E structure on an additive commutative monoid.
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)
:
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)
:
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)
:
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
instance
IsScalarTower.rat
{R : Type u}
{M : Type v}
[Ring R]
[AddCommGroup M]
[Module R M]
[Module ℚ R]
[Module ℚ M]
:
IsScalarTower ℚ R M
instance
SMulCommClass.nnrat
{α : Type u}
{M : Type v}
[Monoid α]
[AddCommMonoid M]
[DistribMulAction α M]
[Module ℚ≥0 M]
:
SMulCommClass ℚ≥0 α M
instance
SMulCommClass.rat
{α : Type u}
{M : Type v}
[Monoid α]
[AddCommGroup M]
[DistribMulAction α M]
[Module ℚ M]
:
SMulCommClass ℚ α M
instance
SMulCommClass.nnrat'
{α : Type u}
{M : Type v}
[Monoid α]
[AddCommMonoid M]
[DistribMulAction α M]
[Module ℚ≥0 M]
:
SMulCommClass α ℚ≥0 M
instance
SMulCommClass.rat'
{α : Type u}
{M : Type v}
[Monoid α]
[AddCommGroup M]
[DistribMulAction α M]
[Module ℚ M]
:
SMulCommClass α ℚ M
@[instance 100]
@[instance 100]