Documentation

@[implicit_reducible]

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

SetLike (Submodule R M) M

@[implicit_reducible]

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

PartialOrder (Submodule R M)

@[simp]

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

s.carrier = ↑s

def Submodule.ofClass {S : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :

Submodule R M

The actual Submodule obtained from an element of a SMulMemClass and AddSubmonoidClass.

Instances For

@[simp]

theorem Submodule.coe_ofClass {S : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :

↑(ofClass s) = ↑s

def Submodule.ofLinearComb {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (C : Set M) (nonempty : C.Nonempty) (linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C) :

Submodule R M

Construct a submodule from closure under two-element linear combinations. I.e., a nonempty set closed under two-element linear combinations is a submodule.

Instances For

@[simp]

theorem Submodule.coe_ofLinearComb {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] (C : Set M) (nonempty : C.Nonempty) (linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C) :

↑(ofLinearComb C nonempty linearComb) = C

@[instance 100]

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

CanLift (Set M) (Submodule R M) SetLike.coe fun (s : Set M) => 0 ∈ s ∧ (∀ {x y : M}, x ∈ s → y ∈ s → x + y ∈ s) ∧ ∀ (r : R) {x : M}, x ∈ s → r • x ∈ s

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

AddSubmonoidClass (Submodule R M) M

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

SMulMemClass (Submodule R M) R M

@[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

@[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

@[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

@[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

@[simp]

theorem Submodule.mk_le_mk {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] {S 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'

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

p = q

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

p = q ↔ ∀ (x : M), x ∈ p ↔ x ∈ q

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.

Instances For

@[simp]

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

↑(p.copy s hs) = s

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) :

S.copy s hs = S

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

Function.Injective toAddSubmonoid

@[simp]

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

p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q

@[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

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

Function.Injective toSubMulAction

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

p.toSubMulAction = q.toSubMulAction ↔ p = q

@[simp]

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

↑p.toSubMulAction = ↑p

@[implicit_reducible]

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

DecidableEq (Submodule R M)

Submodule R M almost never has decidable equality. Given an element m ≠ 0 in M, Submodule R M has decidable equality iff all propositions are decidable. We add a global instance that Submodule R M has decidable equality, coming from the choice axiom, so that we don't have to provide [DecidableEq (Submodule R M)] arguments in lemma statements.

@[implicit_reducible, instance 75]

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.

@[implicit_reducible]

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.

Instances For

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

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

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

x + y ∈ p

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

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

@[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

@[simp]

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

r • x ∈ p ↔ x ∈ p

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

r • x ∈ p ↔ x ∈ p

@[implicit_reducible]

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

Add ↥p

@[implicit_reducible]

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

Zero ↥p

@[implicit_reducible]

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

Inhabited ↥p

@[implicit_reducible]

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

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

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

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

(↑p).Nonempty

@[simp]

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) :

⟨x, h⟩ = 0 ↔ x = 0

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

@[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 y : ↥p) :

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

@[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

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

@[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

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) :

↑⟨x, hx⟩ = x

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

@[implicit_reducible]

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

AddCommMonoid ↥p

@[implicit_reducible]

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

@[implicit_reducible]

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

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

AddSubgroupClass (Submodule R M) M

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

@[reducible]

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.

Instances For

@[simp]

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

↑p.toAddSubgroup = ↑p

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 ∈ p.toAddSubgroup ↔ x ∈ p

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

Function.Injective toAddSubgroup

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

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

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

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

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

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 y : M} :

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

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 y : M} :

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

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

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

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

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 y : M} (hy : y ∈ p) :

x - y ∈ p ↔ x ∈ p

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 y : M} (hx : x ∈ p) :

x - y ∈ p ↔ y ∈ p