Further basic results about modules.

@[deprecated map_natCast_smul]

theorem map_nat_cast_smul {M : Type u_5} {M₂ : Type u_6} [AddCommMonoid M] [AddCommMonoid M₂] {F : Type u_9} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_10) (S : Type u_11) [Semiring R] [Semiring S] [Module R M] [Module S M₂] (x : ℕ) (a : M) : f (↑x • a) = ↑x • f a

Alias of map_natCast_smul.

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

@[deprecated map_inv_natCast_smul]

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

Alias of map_inv_natCast_smul.

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

@[deprecated map_inv_intCast_smul]

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

Alias of map_inv_intCast_smul.

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.

@[deprecated inv_natCast_smul_eq]

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

Alias of inv_natCast_smul_eq.

---

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.

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.

@[deprecated inv_intCast_smul_eq]

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

Alias of inv_intCast_smul_eq.

---

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.

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.

@[deprecated inv_natCast_smul_comm]

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

Alias of inv_natCast_smul_comm.

---

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.

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

@[deprecated inv_intCast_smul_comm]

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

Alias of inv_intCast_smul_comm.

---

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

instance instNoZeroSMulDivisorsNatOfInt_1 {M : Type u_3} [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M

Equations

• ⋯ = ⋯

@[instance 100]

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

• ⋯ = ⋯

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

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

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

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

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

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 : α) : s.indicator (fun (a : α) => r a • f a) a = r a • s.indicator f a

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) : (s.indicator fun (a : α) => r a • f a) = fun (a : α) => r a • s.indicator f a

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 : α) : s.indicator (fun (x : α) => r • f x) a = r • s.indicator f a

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) : (s.indicator fun (x : α) => r • f x) = fun (x : α) => r • s.indicator f x

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 : α) : s.indicator (fun (a : α) => r a • f a) a = s.indicator r a • f a

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) : (s.indicator fun (a : α) => r a • f a) = fun (a : α) => s.indicator r a • f a

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 : α) : s.indicator (fun (x : α) => r x • m) a = s.indicator r a • m

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) : (s.indicator fun (x : α) => r x • m) = fun (x : α) => s.indicator r x • m

theorem Set.smul_indicator_one_apply {α : Type u_1} {R : Type u_2} [MulZeroOneClass R] (s : Set α) (r : R) (a : α) : r • s.indicator 1 a = s.indicator (fun (x : α) => r) a