ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>p : (x : M) → x ∈ Submodule.span R s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>add : ∀ (x : M) (hx : x ∈ Submodule.span R s) (y : M) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯<VAR>smul : ∀ (a : R) (x : M) (hx : x ∈ Submodule.span R s), p x hx → p (a • x) ⋯<VAR>x : M<VAR>hx : x ∈ Submodule.span R s<GOAL>p x hx
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>(Submodule.span R s).toAddSubmonoid = AddSubmonoid.closure (Set.univ • s)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>s : Set M<VAR>p : M → Prop<VAR>h : x ∈ Submodule.span R s<VAR>zero : p 0<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<VAR>smul_mem : ∀ (r : R), ∀ x ∈ s, p (r • x)<GOAL>p x
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>p : (x : M) → x ∈ Submodule.span R s → Prop<VAR>zero : p 0 ⋯<VAR>add : ∀ (x : M) (hx : x ∈ Submodule.span R s) (y : M) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯<VAR>smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯<VAR>x : M<VAR>hx : x ∈ Submodule.span R s<GOAL>p x hx
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.span R (Subtype.val ⁻¹' s) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.span R {x | ↑x ∈ s} = ⊤
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>s : Set M<GOAL>(Submodule.span ℕ s).toAddSubmonoid = AddSubmonoid.closure s
<VAR>M : Type u_4<VAR>AddCommMonoid M<VAR>s : AddSubmonoid M<GOAL>(Submodule.span ℕ ↑s).toAddSubmonoid = s
<VAR>M : Type u_9<VAR>AddCommGroup M<VAR>s : Set M<GOAL>(Submodule.span ℤ s).toAddSubgroup = AddSubgroup.closure s
<VAR>M : Type u_9<VAR>AddCommGroup M<VAR>s : AddSubgroup M<GOAL>(Submodule.span ℤ ↑s).toAddSubgroup = s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.span R ∅ = ⊥
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.span R Set.univ = ⊤
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Set M<GOAL>Submodule.span R (s ∪ t) = Submodule.span R s ⊔ Submodule.span R t
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>s : ι → Set M<GOAL>Submodule.span R (⋃ i, s i) = ⨆ i, Submodule.span R (s i)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_10<VAR>κ : ι → Sort u_9<VAR>s : (i : ι) → κ i → Set M<GOAL>Submodule.span R (⋃ i, ⋃ j, s i j) = ⨆ i, ⨆ j, Submodule.span R (s i j)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>DecidableEq M<VAR>α : Type u_9<VAR>s : Finset α<VAR>f : { x // x ∈ s } → Finset M<GOAL>Submodule.span R ↑(s.attach.biUnion f) = ⨆ x, Submodule.span R ↑(f x)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>s : Set M<GOAL>p ⊔ Submodule.span R s = Submodule.span R (↑p ∪ s)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>s : Set M<GOAL>Submodule.span R s ⊔ p = Submodule.span R (s ∪ ↑p)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.span R s = ⨆ x ∈ s, Submodule.span R {x}
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>v : ι → M<GOAL>Submodule.span R (Set.range v) = ⨆ i, Submodule.span R {v i}
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>r : R<GOAL>Submodule.span R (r • s) ≤ Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>U V W : Set M<VAR>hUV : U ⊆ ↑(Submodule.span R V)<VAR>hVW : V ⊆ ↑(Submodule.span R W)<GOAL>U ⊆ ↑(Submodule.span R W)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>r : R<VAR>hr : IsUnit r<GOAL>Submodule.span R (r • s) = Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>Nonempty ι<VAR>S : ι → Submodule R M<VAR>H : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(iSup S) = ⋃ i, ↑(S i)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>Nonempty ι<VAR>S : ι → Submodule R M<VAR>H : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ iSup S ↔ ∃ i, x ∈ S i
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set (Submodule R M)<VAR>z : M<VAR>hs : s.Nonempty<VAR>hdir : DirectedOn (fun x x_1 => x ≤ x_1) s<GOAL>z ∈ sSup s ↔ ∃ y ∈ s, z ∈ y
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : ℕ →o Submodule R M<GOAL>↑(⨆ k, a k) = ⋃ k, ↑(a k)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>OmegaCompletePartialOrder.Continuous' SetLike.coe
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>a : ℕ →o Submodule R M<VAR>m : M<GOAL>m ∈ ⨆ k, a k ↔ ∃ k, m ∈ a k
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>p p' : Submodule R M<GOAL>x ∈ p ⊔ p' ↔ ∃ y ∈ p, ∃ z ∈ p', y + z = x
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>p p' : Submodule R M<GOAL>x ∈ p ⊔ p' ↔ ∃ y z, ↑y + ↑z = x
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : Codisjoint p p'<VAR>x : M<GOAL>∃ y ∈ p, ∃ z ∈ p', y + z = x
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>↑(p ⊔ p') = ↑p + ↑p'
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>(p ⊔ p').toAddSubmonoid = p.toAddSubmonoid ⊔ p'.toAddSubmonoid
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>(p ⊔ p').toAddSubgroup = p.toAddSubgroup ⊔ p'.toAddSubgroup
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>x ∈ Submodule.span R {x}
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>h : x ≠ 0<GOAL>Nontrivial ↥(Submodule.span R {x})
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : M<GOAL>x ∈ Submodule.span R {y} ↔ ∃ a, a • y = x
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Submodule R M<VAR>v₀ : M<GOAL>s ≤ Submodule.span R {v₀} ↔ ∀ v ∈ s, ∃ r, r • v₀ = v
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>Submodule.span R {x} = ⊤ ↔ ∀ (v : M), ∃ r, r • x = v
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.span R {0} = ⊥
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>y : M<GOAL>↑(Submodule.span R {y}) = Set.range fun x => x • y
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Type u_9<VAR>Monoid S<VAR>SMul S R<VAR>MulAction S M<VAR>IsScalarTower S R M<VAR>r : S<VAR>x : M<GOAL>Submodule.span R {r • x} ≤ Submodule.span R {x}
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>G : Type u_9<VAR>Group G<VAR>SMul G R<VAR>MulAction G M<VAR>IsScalarTower G R M<VAR>g : G<VAR>x : M<GOAL>Submodule.span R {g • x} = Submodule.span R {x}
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>r : R<VAR>hr : IsUnit r<VAR>x : M<GOAL>Submodule.span R {r • x} = Submodule.span R {x}
<VAR>K : Type u_9<VAR>E : Type u_10<VAR>DivisionRing K<VAR>AddCommGroup E<VAR>Module K E<VAR>s : Submodule K E<VAR>x : E<GOAL>Disjoint s (Submodule.span K {x}) ↔ x ∈ s → x = 0
<VAR>K : Type u_9<VAR>E : Type u_10<VAR>DivisionRing K<VAR>AddCommGroup E<VAR>Module K E<VAR>p : Submodule K E<VAR>x : E<VAR>x0 : x ≠ 0<GOAL>Disjoint p (Submodule.span K {x}) ↔ x ∉ p
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y z : M<VAR>hxy : x ∈ Submodule.span R {y}<VAR>hyz : y ∈ Submodule.span R {z}<GOAL>x ∈ Submodule.span R {z}
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>s : Set M<GOAL>Submodule.span R (insert x s) = Submodule.span R {x} ⊔ Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>s : Set M<VAR>h : x ∈ Submodule.span R s<GOAL>Submodule.span R (insert x s) = Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.span R ↑(Submodule.span R s) = Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>s : Set M<VAR>y : M<GOAL>x ∈ Submodule.span R (insert y s) ↔ ∃ a, ∃ z ∈ Submodule.span R s, x = a • y + z
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y z : M<GOAL>z ∈ Submodule.span R {x, y} ↔ ∃ a b, a • x + b • y = z
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>S : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>Semiring S<VAR>SMul R S<VAR>Module S M<VAR>IsScalarTower R S M<GOAL>Submodule.span R s ≤ Submodule.restrictScalars R (Submodule.span S s)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>S : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>Semiring S<VAR>SMul R S<VAR>Module S M<VAR>IsScalarTower R S M<GOAL>↑(Submodule.span R s) ⊆ ↑(Submodule.span S s)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>S : Type u_7<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<VAR>Semiring S<VAR>SMul R S<VAR>Module S M<VAR>IsScalarTower R S M<GOAL>Submodule.span S ↑(Submodule.span R s) = Submodule.span S s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.span R s = ⊥ ↔ ∀ x ∈ s, x = 0
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>Submodule.span R {x} = ⊥ ↔ x = 0
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Submodule.span R 0 = ⊥
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>m : M<VAR>p : Submodule R M<GOAL>Submodule.span R {m} ≤ p ↔ m ∈ p
<VAR>R : Type u_9<VAR>M : Type u_10<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>NoZeroSMulDivisors R M<VAR>x y : M<GOAL>Submodule.span R {x} = Submodule.span R {y} ↔ ∃ z, z • x = y
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>s : Set M<VAR>RingHomSurjective σ₁₂<VAR>f : F<GOAL>Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>s : Set M<VAR>RingHomSurjective σ₁₂<VAR>f : M →ₛₗ[σ₁₂] M₂<GOAL>Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>x : M<VAR>s : Set M<VAR>h : x ∈ Submodule.span R s<GOAL>f x ∈ Submodule.span R₂ (⇑f '' s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>x : M<VAR>s : Set M<VAR>hf : Function.Injective ⇑f<GOAL>f x ∈ Submodule.span R₂ (⇑f '' s) ↔ x ∈ Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>Submodule.map p.subtype (Submodule.span R {x}) = Submodule.span R {↑x}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>RingHomSurjective σ₁₂<VAR>f : F<VAR>x : M<VAR>s : Set M<VAR>h : f x ∉ Submodule.span R₂ (⇑f '' s)<GOAL>x ∉ Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>p : ι → Set M<GOAL>⨆ i, Submodule.span R (p i) = Submodule.span R (⋃ i, p i)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<GOAL>⨆ i, p i = Submodule.span R (⋃ i, ↑(p i))
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<GOAL>(⨆ i, p i).toAddSubmonoid = ⨆ i, (p i).toAddSubmonoid
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, p i<VAR>hp : ∀ (i : ι), ∀ x ∈ p i, C x<VAR>h0 : C 0<VAR>hadd : ∀ (x y : M), C x → C y → C (x + y)<GOAL>C x
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : (x : M) → x ∈ ⨆ i, p i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯<VAR>zero : C 0 ⋯<VAR>add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, p i<GOAL>C x hx
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>CompleteLattice.IsCompactElement (Submodule.span R {x})
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Finset M<GOAL>CompleteLattice.IsCompactElement (Submodule.span R ↑S)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Set M<VAR>h : S.Finite<GOAL>CompleteLattice.IsCompactElement (Submodule.span R S)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>p = sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = Submodule.span R {m}}
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>I : Submodule R M<VAR>a : M<GOAL>I < I ⊔ Submodule.span R {a} ↔ a ∉ I
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>m : M<GOAL>m ∈ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set (Submodule R M)<VAR>m : M<GOAL>m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Set M<VAR>x : M<VAR>hx : x ∈ Submodule.span R S<GOAL>∃ T, ↑T ⊆ S ∧ x ∈ Submodule.span R ↑T
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>q₁ : Submodule R M'<GOAL>↑(p.prod q₁) = ↑p ×ˢ ↑q₁
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>p : Submodule R M<VAR>q : Submodule R M'<VAR>x : M × M'<GOAL>x ∈ p.prod q ↔ x.1 ∈ p ∧ x.2 ∈ q
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>s : Set M<VAR>t : Set M'<GOAL>Submodule.span R (s ×ˢ t) ≤ (Submodule.span R s).prod (Submodule.span R t)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<GOAL>⊤.prod ⊤ = ⊤
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<GOAL>⊥.prod ⊥ = ⊥
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>p p' : Submodule R M<VAR>q q' : Submodule R M'<GOAL>p ≤ p' → q ≤ q' → p.prod q ≤ p'.prod q'
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>q₁ q₁' : Submodule R M'<GOAL>p.prod q₁ ⊓ p'.prod q₁' = (p ⊓ p').prod (q₁ ⊓ q₁')
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>M' : Type u_9<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>q₁ q₁' : Submodule R M'<GOAL>p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s : Set M<GOAL>Submodule.span R (-s) = Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>x y : M<VAR>s : Set M<GOAL>x ∈ Submodule.span R (insert y s) ↔ ∃ a, x + a • y ∈ Submodule.span R s
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>p q r : Submodule R M<VAR>h₁ : IsCompl q r<VAR>h₂ : q ≤ p<GOAL>IsCompl (Submodule.comap p.subtype q) (Submodule.comap p.subtype r)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<GOAL>Submodule.comap f (Submodule.map f p) = p ⊔ LinearMap.ker f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p : Submodule R M<VAR>h : LinearMap.ker f ≤ p<GOAL>Submodule.comap f (Submodule.map f p) = p
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<GOAL>LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_9<VAR>s : Set ι<VAR>p : ι → Submodule R M<GOAL>⨆ i ∈ s, Submodule.comap (⨆ i ∈ s, p i).subtype (p i) = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M₂<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>ι : Type u_9<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>p : ι → Submodule R₂ M₂<VAR>hp : ⨆ i ∈ s, p i = ⊤<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>hf : Function.Surjective ⇑f<GOAL>⨆ i ∈ s, Submodule.comap f (p i) = ⊤
<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>R : Type u_9<VAR>R₂ : Type u_10<VAR>Ring R<VAR>Ring R₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>ι : Type u_11<VAR>s : Set ι<VAR>hs : s.Nonempty<VAR>p : ι → Submodule R₂ M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>hf : LinearMap.range f = ⨆ i ∈ s, p i<GOAL>⨆ i ∈ s, Submodule.comap f (p i) = ⊤
<VAR>K : Type u_3<VAR>V : Type u_6<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>x : V<VAR>p : Submodule K V<GOAL>p ⩿ Submodule.span K {x} ⊔ p
<VAR>K : Type u_3<VAR>V : Type u_6<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>x : V<VAR>p : Submodule K V<VAR>h : x ∉ p<GOAL>p ⋖ Submodule.span K {x} ⊔ p
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>p p' : Submodule R M<GOAL>Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p' ⊔ LinearMap.ker f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>hf : LinearMap.ker f = ⊥<VAR>p p' : Submodule R M<GOAL>Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p'
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>hf : LinearMap.ker f = ⊥<GOAL>Function.Injective (Submodule.map f)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>f : F<VAR>hf : LinearMap.range f = ⊤<VAR>p : Submodule R M<GOAL>Submodule.map f p = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<VAR>b : R<GOAL>(LinearMap.toSpanSingleton R M x) b = b • x
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>Submodule.span R {x} = LinearMap.range (LinearMap.toSpanSingleton R M x)
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>(LinearMap.toSpanSingleton R M x) 1 = x
<VAR>R : Type u_1<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>LinearMap.toSpanSingleton R M 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>e : R<GOAL>IsIdempotentElem (LinearMap.toSpanSingleton R R e) ↔ IsIdempotentElem e
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : Module.End R R<GOAL>IsIdempotentElem (f 1) ↔ IsIdempotentElem f
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>σ₁₂ : R →+* R₂<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>s : Set M<VAR>f g : F<GOAL>Set.EqOn ⇑f ⇑g ↑(Submodule.span R s) ↔ Set.EqOn (⇑f) (⇑g) s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>σ₁₂ : R →+* R₂<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>s : Set M<VAR>f g : F<VAR>H : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(Submodule.span R s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Semiring R₂<VAR>AddCommMonoid M₂<VAR>Module R₂ M₂<VAR>F : Type u_8<VAR>σ₁₂ : R →+* R₂<VAR>FunLike F M M₂<VAR>SemilinearMapClass F σ₁₂ M M₂<VAR>s : Set M<VAR>f g : F<VAR>H : Set.EqOn (⇑f) (⇑g) s<VAR>x : M<VAR>h : x ∈ Submodule.span R s<GOAL>f x = g x