Modules over a ring

In this file we define

• Module R M : an additive commutative monoid M is a Module over a Semiring R if for r : R and x : M their "scalar multiplication" r • x : M is defined, and the operation • satisfies some natural associativity and distributivity axioms similar to those on a ring.

Implementation notes

In typical mathematical usage, our definition of Module corresponds to "semimodule", and the word "module" is reserved for Module R M where R is a Ring and M an AddCommGroup. If R is a Field and M an AddCommGroup, M would be called an R-vector space. Since those assumptions can be made by changing the typeclasses applied to R and M, without changing the axioms in Module, mathlib calls everything a Module.

In older versions of mathlib3, we had separate semimodule and vector_space abbreviations. This caused inference issues in some cases, while not providing any real advantages, so we decided to use a canonical Module typeclass throughout.

Tags

semimodule, module, vector space

theorem Module.ext_iff {R : Type u} {M : Type v} : ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} (x y : Module R M), x = y ↔ SMul.smul = SMul.smul

theorem Module.ext {R : Type u} {M : Type v} : ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} (x y : Module R M), SMul.smul = SMul.smul → x = y

class Module (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] extends DistribMulAction : Type (max u v)

A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring R and an additive monoid of "vectors" M, connected by a "scalar multiplication" operation r • x : M (where r : R and x : M) with some natural associativity and distributivity axioms similar to those on a ring.

• smul : R → M → M
• one_smul : ∀ (b : M), 1 • b = b
• mul_smul : ∀ (x y : R) (b : M), (x * y) • b = x • y • b
• smul_zero : ∀ (a : R), a • 0 = 0
• smul_add : ∀ (a : R) (x y : M), a • (x + y) = a • x + a • y
• add_smul : ∀ (r s : R) (x : M), (r + s) • x = r • x + s • x

  Scalar multiplication distributes over addition from the right.

• zero_smul : ∀ (x : M), 0 • x = 0

  Scalar multiplication by zero gives zero.

instance Module.toMulActionWithZero {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : MulActionWithZero R M

A module over a semiring automatically inherits a MulActionWithZero structure.

Equations

• Module.toMulActionWithZero = let __src := inferInstance; MulActionWithZero.mk ⋯ ⋯

instance AddCommMonoid.natModule {M : Type u_5} [AddCommMonoid M] : Module ℕ M

Equations

• AddCommMonoid.natModule = Module.mk ⋯ ⋯

theorem AddMonoid.End.nat_cast_def {M : Type u_5} [AddCommMonoid M] (n : ℕ) : ↑n = (DistribMulAction.toAddMonoidEnd ℕ M) n

theorem add_smul {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (r : R) (s : R) (x : M) : (r + s) • x = r • x + s • x

theorem Convex.combo_self {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {a : R} {b : R} (h : a + b = 1) (x : M) : a • x + b • x = x

theorem two_smul (R : Type u_2) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : 2 • x = x + x

@[deprecated]

theorem two_smul' (R : Type u_2) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : 2 • x = bit0 x

@[simp]

theorem invOf_two_smul_add_invOf_two_smul (R : Type u_2) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Invertible 2] (x : M) : ⅟2 • x + ⅟2 • x = x

@[reducible]

def Function.Injective.module (R : Type u_2) {M : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [SMul R M₂] (f : M₂ →+ M) (hf : Function.Injective ⇑f) (smul : ∀ (c : R) (x : M₂), f (c • x) = c • f x) : Module R M₂

Pullback a Module structure along an injective additive monoid homomorphism. See note [reducible non-instances].

Equations

• Function.Injective.module R f hf smul = let __src := Function.Injective.distribMulAction f hf smul; Module.mk ⋯ ⋯

def Function.Surjective.module (R : Type u_2) {M : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [SMul R M₂] (f : M →+ M₂) (hf : Function.Surjective ⇑f) (smul : ∀ (c : R) (x : M), f (c • x) = c • f x) : Module R M₂

Pushforward a Module structure along a surjective additive monoid homomorphism.

Equations

• Function.Surjective.module R f hf smul = Module.mk ⋯ ⋯

@[reducible]

def Function.Surjective.moduleLeft {R : Type u_9} {S : Type u_10} {M : Type u_11} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul S M] (f : R →+* S) (hf : Function.Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : Module S M

Push forward the action of R on M along a compatible surjective map f : R →+* S.

See also Function.Surjective.mulActionLeft and Function.Surjective.distribMulActionLeft.

Equations

• Function.Surjective.moduleLeft f hf hsmul = let __src := Function.Surjective.distribMulActionLeft (↑f) hf hsmul; Module.mk ⋯ ⋯

@[reducible]

def Module.compHom {R : Type u_2} {S : Type u_4} (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] (f : S →+* R) : Module S M

Compose a Module with a RingHom, with action f s • m.

See note [reducible non-instances].

Equations

• Module.compHom M f = let __src := MulActionWithZero.compHom M (RingHom.toMonoidWithZeroHom f); let __src_1 := DistribMulAction.compHom M ↑f; Module.mk ⋯ ⋯

@[simp]

theorem Module.toAddMonoidEnd_apply_apply (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (x : R) : ∀ (x_1 : M), ((Module.toAddMonoidEnd R M) x) x_1 = x • x_1

def Module.toAddMonoidEnd (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : R →+* AddMonoid.End M

(•) as an AddMonoidHom.

This is a stronger version of DistribMulAction.toAddMonoidEnd

Equations

• Module.toAddMonoidEnd R M = let __src := DistribMulAction.toAddMonoidEnd R M; { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }

def smulAddHom (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] : R →+ M →+ M

A convenience alias for Module.toAddMonoidEnd as an AddMonoidHom, usually to allow the use of AddMonoidHom.flip.

Equations

• smulAddHom R M = RingHom.toAddMonoidHom (Module.toAddMonoidEnd R M)

@[simp]

theorem smulAddHom_apply {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (r : R) (x : M) : ((smulAddHom R M) r) x = r • x

theorem Module.eq_zero_of_zero_eq_one {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (zero_eq_one : 0 = 1) : x = 0

@[simp]

theorem smul_add_one_sub_smul {M : Type u_5} [AddCommMonoid M] {R : Type u_9} [Ring R] [Module R M] {r : R} {m : M} : r • m + (1 - r) • m = m

instance AddCommGroup.intModule (M : Type u_5) [AddCommGroup M] : Module ℤ M

Equations

• AddCommGroup.intModule M = Module.mk ⋯ ⋯

theorem AddMonoid.End.int_cast_def (M : Type u_5) [AddCommGroup M] (z : ℤ) : ↑z = (DistribMulAction.toAddMonoidEnd ℤ M) z

theorem Convex.combo_eq_smul_sub_add {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] {x : M} {y : M} {a : R} {b : R} (h : a + b = 1) : a • x + b • y = b • (y - x) + x

theorem Module.ext' {R : Type u_9} [Semiring R] {M : Type u_10} [AddCommMonoid M] (P : Module R M) (Q : Module R M) (w : ∀ (r : R) (m : M), r • m = r • m) : P = Q

A variant of Module.ext that's convenient for term-mode.

@[simp]

theorem neg_smul {R : Type u_2} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (r : R) (x : M) : -r • x = -(r • x)

theorem neg_smul_neg {R : Type u_2} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (r : R) (x : M) : -r • -x = r • x

@[simp]

theorem Units.neg_smul {R : Type u_2} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (u : Rˣ) (x : M) : -u • x = -(u • x)

theorem neg_one_smul (R : Type u_2) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (x : M) : -1 • x = -x

theorem sub_smul {R : Type u_2} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (r : R) (s : R) (y : M) : (r - s) • y = r • y - s • y

@[reducible]

def Module.addCommMonoidToAddCommGroup (R : Type u_2) {M : Type u_5} [Ring R] [AddCommMonoid M] [Module R M] : AddCommGroup M

An AddCommMonoid that is a Module over a Ring carries a natural AddCommGroup structure. See note [reducible non-instances].

Equations

• Module.addCommMonoidToAddCommGroup R = let __src := inferInstance; AddCommGroup.mk ⋯

theorem Module.subsingleton (R : Type u_9) (M : Type u_10) [Semiring R] [Subsingleton R] [AddCommMonoid M] [Module R M] : Subsingleton M

A module over a Subsingleton semiring is a Subsingleton. We cannot register this as an instance because Lean has no way to guess R.

theorem Module.nontrivial (R : Type u_9) (M : Type u_10) [Semiring R] [Nontrivial M] [AddCommMonoid M] [Module R M] : Nontrivial R

A semiring is Nontrivial provided that there exists a nontrivial module over this semiring.

instance Semiring.toModule {R : Type u_2} [Semiring R] : Module R R

Equations

• Semiring.toModule = Module.mk ⋯ ⋯

instance Semiring.toOppositeModule {R : Type u_2} [Semiring R] : Module Rᵐᵒᵖ R

Like Semiring.toModule, but multiplies on the right.

Equations

• Semiring.toOppositeModule = let __src := MonoidWithZero.toOppositeMulActionWithZero R; Module.mk ⋯ ⋯

def RingHom.toModule {R : Type u_2} {S : Type u_4} [Semiring R] [Semiring S] (f : R →+* S) : Module R S

A ring homomorphism f : R →+* M defines a module structure by r • x = f r * x.

Equations

• RingHom.toModule f = Module.compHom S f

@[simp]

theorem RingHom.smulOneHom_apply {R : Type u_2} {S : Type u_4} [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] (x : R) : RingHom.smulOneHom x = x • 1

def RingHom.smulOneHom {R : Type u_2} {S : Type u_4} [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] : R →+* S

If the module action of R on S is compatible with multiplication on S, then fun x ↦ x • 1 is a ring homomorphism from R to S.

This is the RingHom version of MonoidHom.smulOneHom.

When R is commutative, usually algebraMap should be preferred.

Equations

• RingHom.smulOneHom = let __spread.0 := MonoidHom.smulOneHom; { toMonoidHom := __spread.0, map_zero' := ⋯, map_add' := ⋯ }

def ringHomEquivModuleIsScalarTower {R : Type u_2} {S : Type u_4} [Semiring R] [Semiring S] : (R →+* S) ≃ { _inst : Module R S // IsScalarTower R S S }

A homomorphism between semirings R and S can be equivalently specified by a R-module structure on S such that S/S/R is a scalar tower.

Equations

• One or more equations did not get rendered due to their size.

theorem nsmul_eq_smul_cast (R : Type u_2) {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (n : ℕ) (b : M) : n • b = ↑n • b

nsmul is equal to any other module structure via a cast.

theorem nat_smul_eq_nsmul {M : Type u_5} [AddCommMonoid M] (h : Module ℕ M) (n : ℕ) (x : M) : SMul.smul n x = n • x

Convert back any exotic ℕ-smul to the canonical instance. This should not be needed since in mathlib all AddCommMonoids should normally have exactly one ℕ-module structure by design.

def AddCommMonoid.natModule.unique {M : Type u_5} [AddCommMonoid M] : Unique (Module ℕ M)

All ℕ-module structures are equal. Not an instance since in mathlib all AddCommMonoid should normally have exactly one ℕ-module structure by design.

Equations

• AddCommMonoid.natModule.unique = { toInhabited := { default := inferInstance }, uniq := ⋯ }

instance AddCommMonoid.nat_isScalarTower {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : IsScalarTower ℕ R M

Equations

• ⋯ = ⋯

theorem zsmul_eq_smul_cast (R : Type u_2) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] (n : ℤ) (b : M) : n • b = ↑n • b

zsmul is equal to any other module structure via a cast.

theorem int_smul_eq_zsmul {M : Type u_5} [AddCommGroup M] (h : Module ℤ M) (n : ℤ) (x : M) : SMul.smul n x = n • x

Convert back any exotic ℤ-smul to the canonical instance. This should not be needed since in mathlib all AddCommGroups should normally have exactly one ℤ-module structure by design.

def AddCommGroup.intModule.unique {M : Type u_5} [AddCommGroup M] : Unique (Module ℤ M)

All ℤ-module structures are equal. Not an instance since in mathlib all AddCommGroup should normally have exactly one ℤ-module structure by design.

Equations

• AddCommGroup.intModule.unique = { toInhabited := { default := inferInstance }, uniq := ⋯ }

theorem map_int_cast_smul {M : Type u_5} {M₂ : Type u_6} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_9} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_10) (S : Type u_11) [Ring R] [Ring S] [Module R M] [Module S M₂] (x : ℤ) (a : M) : f (↑x • a) = ↑x • f a

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

theorem map_inv_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) [DivisionSemiring R] [DivisionSemiring S] [Module R M] [Module S M₂] (n : ℕ) (x : M) : f ((↑n)⁻¹ • x) = (↑n)⁻¹ • f x

theorem map_inv_int_cast_smul {M : Type u_5} {M₂ : Type u_6} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_9} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_10) (S : Type u_11) [DivisionRing R] [DivisionRing S] [Module R M] [Module S M₂] (z : ℤ) (x : M) : f ((↑z)⁻¹ • x) = (↑z)⁻¹ • f x

theorem map_rat_cast_smul {M : Type u_5} {M₂ : Type u_6} [AddCommGroup M] [AddCommGroup M₂] {F : Type u_9} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (R : Type u_10) (S : Type u_11) [DivisionRing R] [DivisionRing S] [Module R M] [Module S M₂] (c : ℚ) (x : M) : f (↑c • x) = ↑c • f x

theorem map_rat_smul {M : Type u_5} {M₂ : Type u_6} [AddCommGroup M] [AddCommGroup M₂] [_instM : Module ℚ M] [_instM₂ : Module ℚ M₂] {F : Type u_9} [FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (c : ℚ) (x : M) : f (c • x) = c • f x

instance instModuleNNRatToSemiringToOrderedSemiringToOrderedCommSemiringInstNNRatCanonicallyOrderedCommSemiring {α : Type u_1} [AddCommMonoid α] [Module ℚ α] : Module NNRat α

A Module over ℚ restricts to a Module over ℚ≥0.

Equations

• instModuleNNRatToSemiringToOrderedSemiringToOrderedCommSemiringInstNNRatCanonicallyOrderedCommSemiring = Module.compHom α NNRat.coeHom

instance subsingleton_rat_module (E : Type u_9) [AddCommGroup E] : Subsingleton (Module ℚ E)

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

Equations

• ⋯ = ⋯

theorem inv_nat_cast_smul_eq {E : Type u_9} (R : Type u_10) (S : Type u_11) [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.

theorem inv_int_cast_smul_eq {E : Type u_9} (R : Type u_10) (S : Type u_11) [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.

theorem inv_nat_cast_smul_comm {α : Type u_9} {E : Type u_10} (R : Type u_11) [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.

theorem inv_int_cast_smul_comm {α : Type u_9} {E : Type u_10} (R : Type u_11) [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

theorem rat_cast_smul_eq {E : Type u_9} (R : Type u_10) (S : Type u_11) [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.

instance AddCommGroup.intIsScalarTower {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] : IsScalarTower ℤ R M

Equations

• ⋯ = ⋯

instance IsScalarTower.rat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] [Module ℚ R] [Module ℚ M] : IsScalarTower ℚ R M

Equations

• ⋯ = ⋯

instance SMulCommClass.rat {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] : SMulCommClass ℚ R M

Equations

• ⋯ = ⋯

instance SMulCommClass.rat' {R : Type u} {M : Type v} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] : SMulCommClass R ℚ M

Equations

• ⋯ = ⋯

NoZeroSMulDivisors

This section defines the NoZeroSMulDivisors class, and includes some tests for the vanishing of elements (especially in modules over division rings).

theorem noZeroSMulDivisors_iff (R : Type u_9) (M : Type u_10) [Zero R] [Zero M] [SMul R M] : NoZeroSMulDivisors R M ↔ ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

class NoZeroSMulDivisors (R : Type u_9) (M : Type u_10) [Zero R] [Zero M] [SMul R M] : Prop

NoZeroSMulDivisors R M states that a scalar multiple is 0 only if either argument is 0. This is a version of saying that M is torsion free, without assuming R is zero-divisor free.

The main application of NoZeroSMulDivisors R M, when M is a module, is the result smul_eq_zero: a scalar multiple is 0 iff either argument is 0.

It is a generalization of the NoZeroDivisors class to heterogeneous multiplication.

• eq_zero_or_eq_zero_of_smul_eq_zero : ∀ {c : R} {x : M}, c • x = 0 → c = 0 ∨ x = 0

  If scalar multiplication yields zero, either the scalar or the vector was zero.

theorem Function.Injective.noZeroSMulDivisors {R : Type u_9} {M : Type u_10} {N : Type u_11} [Zero R] [Zero M] [Zero N] [SMul R M] [SMul R N] [NoZeroSMulDivisors R N] (f : M → N) (hf : Function.Injective f) (h0 : f 0 = 0) (hs : ∀ (c : R) (x : M), f (c • x) = c • f x) : NoZeroSMulDivisors R M

Pullback a NoZeroSMulDivisors instance along an injective function.

instance NoZeroDivisors.toNoZeroSMulDivisors {R : Type u_2} [Zero R] [Mul R] [NoZeroDivisors R] : NoZeroSMulDivisors R R

Equations

• ⋯ = ⋯

theorem smul_ne_zero {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMul R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) (hx : x ≠ 0) : c • x ≠ 0

@[simp]

theorem smul_eq_zero {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} : c • x = 0 ↔ c = 0 ∨ x = 0

theorem smul_ne_zero_iff {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} : c • x ≠ 0 ↔ c ≠ 0 ∧ x ≠ 0

theorem smul_eq_zero_iff_left {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hx : x ≠ 0) : c • x = 0 ↔ c = 0

theorem smul_eq_zero_iff_right {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) : c • x = 0 ↔ x = 0

theorem smul_ne_zero_iff_left {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hx : x ≠ 0) : c • x ≠ 0 ↔ c ≠ 0

theorem smul_ne_zero_iff_right {R : Type u_2} {M : Type u_5} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {c : R} {x : M} (hc : c ≠ 0) : c • x ≠ 0 ↔ x ≠ 0

theorem Nat.noZeroSMulDivisors (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] : NoZeroSMulDivisors ℕ M

theorem two_nsmul_eq_zero (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : 2 • v = 0 ↔ v = 0

theorem CharZero.of_module (R : Type u_2) [Semiring R] (M : Type u_9) [AddCommMonoidWithOne M] [CharZero M] [Module R M] : CharZero R

If M is an R-module with one and M has characteristic zero, then R has characteristic zero as well. Usually M is an R-algebra.

theorem smul_right_injective {R : Type u_2} (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) : Function.Injective fun (x : M) => c • x

theorem smul_right_inj {R : Type u_2} {M : Type u_5} [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) {x : M} {y : M} : c • x = c • y ↔ x = y

theorem self_eq_neg (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : v = -v ↔ v = 0

theorem neg_eq_self (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : -v = v ↔ v = 0

theorem self_ne_neg (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : v ≠ -v ↔ v ≠ 0

theorem neg_ne_self (R : Type u_2) (M : Type u_5) [Semiring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] {v : M} : -v ≠ v ↔ v ≠ 0

theorem smul_left_injective (R : Type u_2) {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} (hx : x ≠ 0) : Function.Injective fun (c : R) => c • x

instance instNoZeroSMulDivisorsNatToZeroLinearOrderedCommMonoidWithZeroToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToNatSMulToAddMonoidToSubNegMonoidToAddGroup {M : Type u_5} [AddCommGroup M] [NoZeroSMulDivisors ℤ M] : NoZeroSMulDivisors ℕ M

Equations

• ⋯ = ⋯

theorem NoZeroSMulDivisors.int_of_charZero (R : Type u_2) (M : Type u_5) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] [CharZero R] : NoZeroSMulDivisors ℤ M

theorem CharZero.of_noZeroSMulDivisors (R : Type u_2) (M : Type u_5) [Ring R] [AddCommGroup M] [Module R M] [Nontrivial M] [NoZeroSMulDivisors ℤ M] : CharZero R

Only a ring of characteristic zero can can have a non-trivial module without additive or scalar torsion.

instance GroupWithZero.toNoZeroSMulDivisors {R : Type u_2} {M : Type u_5} [GroupWithZero R] [AddMonoid M] [DistribMulAction R M] : NoZeroSMulDivisors R M

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

Equations

• ⋯ = ⋯

instance RatModule.noZeroSMulDivisors {M : Type u_5} [AddCommGroup M] [Module ℚ M] : NoZeroSMulDivisors ℤ M

Equations

• ⋯ = ⋯

theorem Nat.smul_one_eq_coe {R : Type u_9} [Semiring R] (m : ℕ) : m • 1 = ↑m

theorem Int.smul_one_eq_coe {R : Type u_9} [Ring R] (m : ℤ) : m • 1 = ↑m

theorem Function.support_smul_subset_left {α : Type u_1} {R : Type u_2} {M : Type u_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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

theorem Set.indicator_smul {α : Type u_1} {R : Type u_2} {M : Type u_5} [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

theorem Set.indicator_const_smul_apply {α : Type u_1} {R : Type u_2} {M : Type u_5} [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

theorem Set.indicator_const_smul {α : Type u_1} {R : Type u_2} {M : Type u_5} [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

theorem Set.indicator_smul_apply_left {α : Type u_1} {R : Type u_2} {M : Type u_5} [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

theorem Set.indicator_smul_left {α : Type u_1} {R : Type u_2} {M : Type u_5} [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

theorem Set.indicator_smul_const_apply {α : Type u_1} {R : Type u_2} {M : Type u_5} [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

theorem Set.indicator_smul_const {α : Type u_1} {R : Type u_2} {M : Type u_5} [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