# Further basic results about modules. #

@[deprecated map_natCast_smul]
theorem map_nat_cast_smul {M : Type u_5} {M₂ : Type u_6} [] [] {F : Type u_9} [FunLike F M M₂] [] (f : F) (R : Type u_10) (S : Type u_11) [] [] [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} [] [] {F : Type u_5} [FunLike F M M₂] [] (f : F) (R : Type u_6) (S : Type u_7) [] [] [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} [] [] {F : Type u_5} [FunLike F M M₂] [] (f : F) (R : Type u_6) (S : Type u_7) [] [] [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} [] [] {F : Type u_5} [FunLike F M M₂] [] (f : F) (R : Type u_6) (S : Type u_7) [] [] [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} [] [] {F : Type u_5} [FunLike F M M₂] [] (f : F) (R : Type u_6) (S : Type u_7) [] [] [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) [] [] [] [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) [] [] [] [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) [] [] [] [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) [] [] [] [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) [] [] [] [Module R 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) [] [] [] [Module R 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) [] [] [] [Module R 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) [] [] [] [Module R 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} [] [] :
Equations
• =
@[instance 100]
instance GroupWithZero.toNoZeroSMulDivisors {R : Type u_2} {M : Type u_3} [] [] [] :

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] [] (f : αR) (g : αM) :
theorem Function.support_smul_subset_right {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero M] [] (f : αR) (g : αM) :
theorem Function.support_const_smul_of_ne_zero {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [] [] (c : R) (g : αM) (hc : c 0) :
theorem Function.support_smul {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero R] [Zero M] [] [] (f : αR) (g : αM) :
theorem Function.support_const_smul_subset {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero M] [] (a : R) (f : αM) :
theorem Set.indicator_smul_apply {α : Type u_1} {R : Type u_2} {M : Type u_3} [Zero 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] [] (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] [] (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] [] (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] [] (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] [] (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] [] (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] [] (s : Set α) (r : αR) (m : M) :
(s.indicator fun (x : α) => r x m) = fun (x : α) => s.indicator r x m