Polyhedral cones

...

def Submodule.IsLineOrBot {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (S : Submodule R M) : Prop

Equations

• S.IsLineOrBot = ∃ (x : M), Submodule.span R {x} = S

structure Submodule.LineOrBot (R : Type u_7) [Semiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] extends Submodule R M : Type u_8

• 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
• isPreLine : self.IsLineOrBot

instance Submodule.LineOrBot.instCoe {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] : Coe (LineOrBot R M) (Submodule R M)

Equations

• Submodule.LineOrBot.instCoe = { coe := Submodule.LineOrBot.toSubmodule }

def Submodule.LineOrBot.of_isLineOrBot {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] {S : Submodule R M} (hS : S.IsLineOrBot) : LineOrBot R M

Equations

• Submodule.LineOrBot.of_isLineOrBot hS = { toSubmodule := S, isPreLine := hS }

theorem Submodule.LineOrBot.toSubmodule_injective {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] : Function.Injective toSubmodule

instance Submodule.LineOrBot.instSetLike {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] : SetLike (LineOrBot R M) M

Equations

• Submodule.LineOrBot.instSetLike = { coe := fun (C : Submodule.LineOrBot R M) => ↑C.toSubmodule, coe_injective' := ⋯ }

@[simp]

theorem Submodule.LineOrBot.coe_toSubmodule {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (C : LineOrBot R M) : ↑C.toSubmodule = ↑C

def Submodule.IsLine {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (S : Submodule R M) : Prop

Equations

• S.IsLine = ∃ (x : M), x ≠ 0 ∧ Submodule.span R {x} = S

structure Submodule.Line (R : Type u_7) [Semiring R] (M : Type u_8) [AddCommMonoid M] [Module R M] extends Submodule R M : Type u_8

• 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
• isLine : self.IsLine

instance Submodule.Line.instCoe {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] : Coe (Line R M) (Submodule R M)

Equations

• Submodule.Line.instCoe = { coe := Submodule.Line.toSubmodule }

def Submodule.Line.of_isLine {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] {S : Submodule R M} (hS : S.IsLine) : Line R M

Equations

• Submodule.Line.of_isLine hS = { toSubmodule := S, isLine := hS }

theorem Submodule.Line.toSubmodule_injective {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] : Function.Injective toSubmodule

instance Submodule.Line.instSetLike {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] : SetLike (Line R M) M

Equations

• Submodule.Line.instSetLike = { coe := fun (C : Submodule.Line R M) => ↑C.toSubmodule, coe_injective' := ⋯ }

@[simp]

theorem Submodule.Line.coe_toSubmodule {R : Type u_7} [Semiring R] {M : Type u_8} [AddCommMonoid M] [Module R M] (C : Line R M) : ↑C.toSubmodule = ↑C