Submodules of a module #

In this file we define

Submodule R M : a subset of a Module M that contains zero and is closed with respect to addition and scalar multiplication.
Subspace k M : an abbreviation for Submodule assuming that k is a Field.

Tags #

submodule, subspace, linear map

structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] extends AddSubmonoid :

A submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.

carrier : Set M
add_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
zero_mem' : 0 ∈ self.carrier
smul_mem' : ∀ (c : R) {x : M}, x ∈ self.carrier → c • x ∈ self.carrier
The carrier set is closed under scalar multiplication.

Instances For

source

@[reducible]

abbrev Submodule.toSubMulAction {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (self : Submodule R M) :

SubMulAction R M

Reinterpret a Submodule as a SubMulAction.

Equations

Submodule.toSubMulAction self = { carrier := self.carrier, smul_mem' := ⋯ }

Instances For

source

instance Submodule.setLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

SetLike (Submodule R M) M

Equations

Submodule.setLike = { coe := fun (s : Submodule R M) => s.carrier, coe_injective' := ⋯ }

source

instance Submodule.addSubmonoidClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

AddSubmonoidClass (Submodule R M) M

Equations

⋯ = ⋯

source

instance Submodule.smulMemClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

SMulMemClass (Submodule R M) R M

Equations

⋯ = ⋯

source

@[simp]

theorem Submodule.mem_toAddSubmonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (x : M) :

x ∈ p.toAddSubmonoid ↔ x ∈ p

source

@[simp]

theorem Submodule.mem_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {S : AddSubmonoid M} {x : M} (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier) :

x ∈ { toAddSubmonoid := S, smul_mem' := h } ↔ x ∈ S

source

@[simp]

theorem Submodule.coe_set_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : AddSubmonoid M) (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier) :

↑{ toAddSubmonoid := S, smul_mem' := h } = ↑S

source

@[simp]

theorem Submodule.eta {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (h : ∀ (c : R) {x : M}, x ∈ p.carrier → c • x ∈ p.carrier) :

{ toAddSubmonoid := p.toAddSubmonoid, smul_mem' := h } = p

source

@[simp]

theorem Submodule.mk_le_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {S : AddSubmonoid M} {S' : AddSubmonoid M} (h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier) (h' : ∀ (c : R) {x : M}, x ∈ S'.carrier → c • x ∈ S'.carrier) :

{ toAddSubmonoid := S, smul_mem' := h } ≤ { toAddSubmonoid := S', smul_mem' := h' } ↔ S ≤ S'

source

theorem Submodule.ext {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (h : ∀ (x : M), x ∈ p ↔ x ∈ q) :

p = q

source

@[simp]

theorem Submodule.carrier_inj {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :

p.carrier = q.carrier ↔ p = q

source

def Submodule.copy {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (s : Set M) (hs : s = ↑p) :

Submodule R M

Copy of a submodule with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

Submodule.copy p s hs = { toAddSubmonoid := { toAddSubsemigroup := { carrier := s, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }

Instances For

source

@[simp]

theorem Submodule.coe_copy {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) (s : Set M) (hs : s = ↑S) :

↑(Submodule.copy S s hs) = s

source

theorem Submodule.copy_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) (s : Set M) (hs : s = ↑S) :

Submodule.copy S s hs = S

source

theorem Submodule.toAddSubmonoid_injective {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

Function.Injective Submodule.toAddSubmonoid

source

@[simp]

theorem Submodule.toAddSubmonoid_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :

p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q

source

theorem Submodule.toAddSubmonoid_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

StrictMono Submodule.toAddSubmonoid

source

theorem Submodule.toAddSubmonoid_le {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :

p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q

source

theorem Submodule.toAddSubmonoid_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

Monotone Submodule.toAddSubmonoid

source

@[simp]

theorem Submodule.coe_toAddSubmonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

↑p.toAddSubmonoid = ↑p

source

theorem Submodule.toSubMulAction_injective {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

Function.Injective Submodule.toSubMulAction

source

theorem Submodule.toSubMulAction_eq {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :

Submodule.toSubMulAction p = Submodule.toSubMulAction q ↔ p = q

source

theorem Submodule.toSubMulAction_strictMono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

StrictMono Submodule.toSubMulAction

source

theorem Submodule.toSubMulAction_mono {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] :

Monotone Submodule.toSubMulAction

source

@[simp]

theorem Submodule.coe_toSubMulAction {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

↑(Submodule.toSubMulAction p) = ↑p

source

instance SMulMemClass.toModule {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] [SMulMemClass A R M] (S' : A) :

Module R ↥S'

A submodule of a Module is a Module.

Equations

SMulMemClass.toModule S' = Function.Injective.module R (AddSubmonoidClass.subtype S') ⋯ ⋯

source

def SMulMemClass.toModule' (S : Type u_2) (R' : Type u_3) (R : Type u_4) (A : Type u_5) [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Semiring R'] [SMul R' R] [Module R' A] [IsScalarTower R' R A] [SetLike S A] [AddSubmonoidClass S A] [SMulMemClass S R A] (s : S) :

Module R' ↥s

This can't be an instance because Lean wouldn't know how to find R, but we can still use this to manually derive Module on specific types.

Equations

SMulMemClass.toModule' S R' R A s = SMulMemClass.toModule s

Instances For

source

theorem Submodule.mem_carrier {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} :

x ∈ p.carrier ↔ x ∈ ↑p

source

@[simp]

theorem Submodule.zero_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

0 ∈ p

source

theorem Submodule.add_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (h₁ : x ∈ p) (h₂ : y ∈ p) :

x + y ∈ p

source

theorem Submodule.smul_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} (r : R) (h : x ∈ p) :

r • x ∈ p

source

theorem Submodule.smul_of_tower_mem {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (h : x ∈ p) :

r • x ∈ p

source

theorem Submodule.sum_mem {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {t : Finset ι} {f : ι → M} :

(∀ c ∈ t, f c ∈ p) → (Finset.sum t fun (i : ι) => f i) ∈ p

source

theorem Submodule.sum_smul_mem {R : Type u} {M : Type v} {ι : Type w} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {t : Finset ι} {f : ι → M} (r : ι → R) (hyp : ∀ c ∈ t, f c ∈ p) :

(Finset.sum t fun (i : ι) => r i • f i) ∈ p

source

@[simp]

theorem Submodule.smul_mem_iff' {G : Type u''} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} [Group G] [MulAction G M] [SMul G R] [IsScalarTower G R M] (g : G) :

g • x ∈ p ↔ x ∈ p

source

instance Submodule.add {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

Add ↥p

Equations

Submodule.add p = { add := fun (x y : ↥p) => { val := ↑x + ↑y, property := ⋯ } }

source

instance Submodule.zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

Zero ↥p

Equations

Submodule.zero p = { zero := { val := 0, property := ⋯ } }

source

instance Submodule.inhabited {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

Inhabited ↥p

Equations

Submodule.inhabited p = { default := 0 }

source

instance Submodule.smul {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] :

SMul S ↥p

Equations

Submodule.smul p = { smul := fun (c : S) (x : ↥p) => { val := c • ↑x, property := ⋯ } }

source

instance Submodule.isScalarTower {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] :

IsScalarTower S R ↥p

Equations

⋯ = ⋯

source

instance Submodule.isScalarTower' {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {S' : Type u_1} [SMul S R] [SMul S M] [SMul S' R] [SMul S' M] [SMul S S'] [IsScalarTower S' R M] [IsScalarTower S S' M] [IsScalarTower S R M] :

IsScalarTower S S' ↥p

Equations

⋯ = ⋯

source

instance Submodule.isCentralScalar {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [SMul S R] [SMul S M] [IsScalarTower S R M] [SMul Sᵐᵒᵖ R] [SMul Sᵐᵒᵖ M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] :

IsCentralScalar S ↥p

Equations

⋯ = ⋯

source

theorem Submodule.nonempty {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

Set.Nonempty ↑p

source

theorem Submodule.mk_eq_zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {x : M} (h : x ∈ p) :

{ val := x, property := h } = 0 ↔ x = 0

source

theorem Submodule.coe_eq_zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {x : ↥p} :

↑x = 0 ↔ x = 0

source

@[simp]

theorem Submodule.coe_add {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : ↥p) (y : ↥p) :

↑(x + y) = ↑x + ↑y

source

@[simp]

theorem Submodule.coe_zero {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} :

↑0 = 0

source

theorem Submodule.coe_smul {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (r : R) (x : ↥p) :

↑(r • x) = r • ↑x

source

@[simp]

theorem Submodule.coe_smul_of_tower {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} [SMul S R] [SMul S M] [IsScalarTower S R M] (r : S) (x : ↥p) :

↑(r • x) = r • ↑x

source

theorem Submodule.coe_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : M) (hx : x ∈ p) :

↑{ val := x, property := hx } = x

source

theorem Submodule.coe_mem {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} (x : ↥p) :

↑x ∈ p

source

instance Submodule.addCommMonoid {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

AddCommMonoid ↥p

Equations

Submodule.addCommMonoid p = let __src := AddSubmonoid.toAddCommMonoid p.toAddSubmonoid; AddCommMonoid.mk ⋯

source

instance Submodule.module' {S : Type u'} {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :

Module S ↥p

Equations

Submodule.module' p = let __src := let_fun this := SubMulAction.mulAction' (Submodule.toSubMulAction p); this; Module.mk ⋯ ⋯

source

instance Submodule.module {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) :

Module R ↥p

Equations

Submodule.module p = Submodule.module' p

source

instance Submodule.noZeroSMulDivisors {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) [NoZeroSMulDivisors R M] :

NoZeroSMulDivisors R ↥p

Equations

⋯ = ⋯

Additive actions by `Submodule`s #

These instances transfer the action by an element m : M of an R-module M written as m +ᵥ a onto the action by an element s : S of a submodule S : Submodule R M such that s +ᵥ a = (s : M) +ᵥ a. These instances work particularly well in conjunction with AddGroup.toAddAction, enabling s +ᵥ m as an alias for ↑s + m.

source

instance Submodule.instVAddSubtypeMemSubmoduleInstMembershipSetLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [VAdd M α] :

VAdd (↥p) α

Equations

Submodule.instVAddSubtypeMemSubmoduleInstMembershipSetLike p = AddSubmonoid.vadd p.toAddSubmonoid

source

instance Submodule.vaddCommClass {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} {β : Type u_2} [VAdd M β] [VAdd α β] [VAddCommClass M α β] :

VAddCommClass (↥p) α β

Equations

⋯ = ⋯

source

instance Submodule.instFaithfulVAddSubtypeMemSubmoduleInstMembershipSetLikeInstVAddSubtypeMemSubmoduleInstMembershipSetLike {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} (p : Submodule R M) {α : Type u_1} [VAdd M α] [FaithfulVAdd M α] :

FaithfulVAdd (↥p) α

Equations

⋯ = ⋯

source

theorem Submodule.vadd_def {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] {module_M : Module R M} {p : Submodule R M} {α : Type u_1} [VAdd M α] (g : ↥p) (m : α) :

g +ᵥ m = ↑g +ᵥ m

source

instance Submodule.addSubgroupClass {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [Module R M] :

AddSubgroupClass (Submodule R M) M

Equations

⋯ = ⋯

source

theorem Submodule.neg_mem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} (hx : x ∈ p) :

-x ∈ p

source

def Submodule.toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

AddSubgroup M

Reinterpret a submodule as an additive subgroup.

Equations

Submodule.toAddSubgroup p = let __src := p.toAddSubmonoid; { toAddSubmonoid := __src, neg_mem' := ⋯ }

Instances For

source

@[simp]

theorem Submodule.coe_toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

↑(Submodule.toAddSubgroup p) = ↑p

source

@[simp]

theorem Submodule.mem_toAddSubgroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} :

x ∈ Submodule.toAddSubgroup p ↔ x ∈ p

source

theorem Submodule.toAddSubgroup_injective {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :

Function.Injective Submodule.toAddSubgroup

source

@[simp]

theorem Submodule.toAddSubgroup_eq {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (p' : Submodule R M) :

Submodule.toAddSubgroup p = Submodule.toAddSubgroup p' ↔ p = p'

source

theorem Submodule.toAddSubgroup_strictMono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :

StrictMono Submodule.toAddSubgroup

source

theorem Submodule.toAddSubgroup_le {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (p' : Submodule R M) :

Submodule.toAddSubgroup p ≤ Submodule.toAddSubgroup p' ↔ p ≤ p'

source

theorem Submodule.toAddSubgroup_mono {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} :

Monotone Submodule.toAddSubgroup

source

theorem Submodule.sub_mem {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :

x ∈ p → y ∈ p → x - y ∈ p

source

theorem Submodule.neg_mem_iff {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} :

-x ∈ p ↔ x ∈ p

source

theorem Submodule.add_mem_iff_left {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :

y ∈ p → (x + y ∈ p ↔ x ∈ p)

source

theorem Submodule.add_mem_iff_right {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} :

x ∈ p → (x + y ∈ p ↔ y ∈ p)

source

theorem Submodule.coe_neg {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (x : ↥p) :

↑(-x) = -↑x

source

theorem Submodule.coe_sub {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) (x : ↥p) (y : ↥p) :

↑(x - y) = ↑x - ↑y

source

theorem Submodule.sub_mem_iff_left {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (hy : y ∈ p) :

x - y ∈ p ↔ x ∈ p

source

theorem Submodule.sub_mem_iff_right {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) {x : M} {y : M} (hx : x ∈ p) :

x - y ∈ p ↔ y ∈ p

source

instance Submodule.addCommGroup {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

AddCommGroup ↥p

Equations

Submodule.addCommGroup p = let __src := AddSubgroup.toAddCommGroup (Submodule.toAddSubgroup p); AddCommGroup.mk ⋯

source

theorem Submodule.neg_coe {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] {module_M : Module R M} (p : Submodule R M) :

-↑p = ↑p

source

theorem Submodule.not_mem_of_ortho {R : Type u} {M : Type v} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) :

x ∉ N

source

theorem Submodule.ne_zero_of_ortho {R : Type u} {M : Type v} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] {x : M} {N : Submodule R M} (ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0) :

x ≠ 0

source