Documentation

Mathlib.Algebra.Module.Basic

Further basic results about modules. #

source
theorem map_inv_natCast_smul {M : Type u_3} {M₂ : Type u_4} [AddCommMonoid M] [AddCommMonoid M₂] {F : Type u_5} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [DivisionSemiring R] [DivisionSemiring S] [Module R M] [Module S M₂] (n : ℕ) (x : M) :
f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x
source
theorem map_inv_intCast_smul {M : Type u_3} {M₂ : Type u_4} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_5} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [DivisionRing R] [DivisionRing S] [Module R M] [Module S M₂] (z : ℤ) (x : M) :
f ((↑z)⁻¹ • x) = (↑z)⁻¹ • f x
source
theorem map_ratCast_smul {M : Type u_3} {M₂ : Type u_4} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_5} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_6) (S : Type u_7) [DivisionRing R] [DivisionRing S] [Module R M] [Module S M₂] (c : ℚ) (x : M) :
f (↑c • x) = ↑c • f x
source
theorem map_rat_smul {M : Type u_3} {M₂ : Type u_4} [AddCommGroup M] [AddCommGroup M₂] [_instM : Module ℚ M] [_instM₂ : Module ℚ M₂] {F : Type u_5} [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_5) [AddCommGroup E] :
Subsingleton (Module ℚ E)

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

Equations
  • ⋯ = ⋯
source
theorem inv_natCast_smul_eq {E : Type u_5} (R : Type u_6) (S : Type u_7) [AddCommMonoid E] [DivisionSemiring R] [DivisionSemiring S] [Module R E] [Module S E] (n : ℕ) (x : E) :
(↑n)⁻¹ • x = (↑n)⁻¹ • x

If E is a vector space over two division semirings R and S, then scalar multiplications agree on inverses of natural numbers in R and S.

source
theorem inv_intCast_smul_eq {E : Type u_5} (R : Type u_6) (S : Type u_7) [AddCommGroup E] [DivisionRing R] [DivisionRing S] [Module R E] [Module S E] (n : ℤ) (x : E) :
(↑n)⁻¹ • x = (↑n)⁻¹ • x

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

source
theorem inv_natCast_smul_comm {α : Type u_5} {E : Type u_6} (R : Type u_7) [AddCommMonoid E] [DivisionSemiring R] [Monoid α] [Module R E] [DistribMulAction α E] (n : ℕ) (s : α) (x : E) :
(↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x

If E is a vector space over a division semiring R and has a monoid action by α, then that action commutes by scalar multiplication of inverses of natural numbers in R.

source
theorem inv_intCast_smul_comm {α : Type u_5} {E : Type u_6} (R : Type u_7) [AddCommGroup E] [DivisionRing R] [Monoid α] [Module R E] [DistribMulAction α E] (n : ℤ) (s : α) (x : E) :
(↑n)⁻¹ • s • x = s • (↑n)⁻¹ • x

If E is a vector space over a division ring R and has a monoid action by α, then that action commutes by scalar multiplication of inverses of integers in R

source
theorem ratCast_smul_eq {E : Type u_5} (R : Type u_6) (S : Type u_7) [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.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 instNoZeroSMulDivisorsNatToZeroInstLinearOrderedCommMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToNatSMulToAddMonoidToSubNegMonoidToAddGroup_1 {M : Type u_3} [AddCommGroup M] [NoZeroSMulDivisors ℤ M] :
NoZeroSMulDivisors ℕ M
Equations
  • ⋯ = ⋯
source
instance GroupWithZero.toNoZeroSMulDivisors {R : Type u_2} {M : Type u_3} [GroupWithZero R] [AddMonoid M] [DistribMulAction R M] :
NoZeroSMulDivisors R M

This instance applies to DivisionSemirings, in particular NNReal and NNRat.

Equations
  • ⋯ = ⋯
source
instance RatModule.noZeroSMulDivisors {M : Type u_3} [AddCommGroup M] [Module ℚ M] :
NoZeroSMulDivisors ℤ M
Equations
  • ⋯ = ⋯
source
theorem Function.support_smul_subset_left {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] (f : α → R) (g : α → M) :
Function.support (f • g) ⊆ Function.support f
source
theorem Function.support_smul_subset_right {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero M] [SMulZeroClass R M] (f : α → R) (g : α → M) :
Function.support (f • g) ⊆ Function.support g
source
theorem Function.support_const_smul_of_ne_zero {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] (c : R) (g : α → M) (hc : c ≠ 0) :
Function.support (c • g) = Function.support g
source
theorem Function.support_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] (f : α → R) (g : α → M) :
Function.support (f • g) = Function.support f ∩ Function.support g
source
theorem Function.support_const_smul_subset {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero M] [SMulZeroClass R M] (a : R) (f : α → M) :
Function.support (a • f) ⊆ Function.support f
source
theorem Set.indicator_smul_apply {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero M] [SMulZeroClass R M] (s : Set α) (r : α → R) (f : α → M) (a : α) :
Set.indicator s (fun (a : α) => r a • f a) a = r a • Set.indicator s f a
source
theorem Set.indicator_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero M] [SMulZeroClass R M] (s : Set α) (r : α → R) (f : α → M) :
(Set.indicator s fun (a : α) => r a • f a) = fun (a : α) => r a • Set.indicator s f a
source
theorem Set.indicator_const_smul_apply {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero M] [SMulZeroClass R M] (s : Set α) (r : R) (f : α → M) (a : α) :
Set.indicator s (fun (x : α) => r • f x) a = r • Set.indicator s f a
source
theorem Set.indicator_const_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero M] [SMulZeroClass R M] (s : Set α) (r : R) (f : α → M) :
(Set.indicator s fun (x : α) => r • f x) = fun (x : α) => r • Set.indicator s f x
source
theorem Set.indicator_smul_apply_left {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] (s : Set α) (r : α → R) (f : α → M) (a : α) :
Set.indicator s (fun (a : α) => r a • f a) a = Set.indicator s r a • f a
source
theorem Set.indicator_smul_left {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] (s : Set α) (r : α → R) (f : α → M) :
(Set.indicator s fun (a : α) => r a • f a) = fun (a : α) => Set.indicator s r a • f a
source
theorem Set.indicator_smul_const_apply {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] (s : Set α) (r : α → R) (m : M) (a : α) :
Set.indicator s (fun (x : α) => r x • m) a = Set.indicator s r a • m
source
theorem Set.indicator_smul_const {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [SMulWithZero R M] (s : Set α) (r : α → R) (m : M) :
(Set.indicator s fun (x : α) => r x • m) = fun (x : α) => Set.indicator s r x • m