ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>AddCommGroup V'<VAR>Module K V<VAR>Module K V'<VAR>p : Submodule K V<VAR>f : ↥p →ₗ[K] V'<GOAL>∃ g, g ∘ₗ p.subtype = f
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<VAR>hp : p < ⊤<GOAL>∃ f, f ≠ 0 ∧ p ≤ LinearMap.ker f
<VAR>K : Type u_3<VAR>V : Type u_4<VAR>DivisionRing K<VAR>AddCommGroup V<VAR>Module K V<VAR>p : Submodule K V<GOAL>Nonempty (((V ⧸ p) × ↥p) ≃ₗ[K] V)
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>R : Type u_3<VAR>Field K<VAR>Finite K<VAR>CommRing R<VAR>Finite ι<VAR>Algebra K R<VAR>Algebra.IsAlgebraic K R<VAR>ps : ι → MvPolynomial ι R<VAR>hinj : Function.Injective fun v i => (MvPolynomial.eval v) (ps i)<GOAL>Function.Surjective fun v i => (MvPolynomial.eval v) (ps i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>y : M<GOAL>(Module.preReflection x f) y = y - f y • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>h : f x = 2<GOAL>(Module.preReflection x f) x = -x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>h : f x = 2<GOAL>Function.Involutive ⇑(Module.preReflection x f)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>y : M<VAR>g : Module.Dual R M<VAR>h : f x = 2<GOAL>Module.preReflection ((Module.preReflection x f) y) ((Module.preReflection f ((Module.Dual.eval R M) x)) g) = Module.preReflection x f ∘ₗ Module.preReflection y g ∘ₗ Module.preReflection x f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>y : M<VAR>h : f x = 2<GOAL>(Module.reflection h) y = y - f y • x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>h : f x = 2<GOAL>(Module.reflection h) x = -x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>h : f x = 2<GOAL>Function.Involutive ⇑(Module.reflection h)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>h : f x = 2<GOAL>(Module.reflection h).symm = Module.reflection h
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>Φ : Set M<VAR>h : f x = 2<GOAL>Set.InvOn (⇑(Module.reflection h)) (⇑(Module.reflection h)) Φ Φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>Φ : Set M<VAR>h : f x = 2<VAR>h' : Set.MapsTo (⇑(Module.reflection h)) Φ Φ<GOAL>Set.BijOn (⇑(Module.reflection h)) Φ Φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>CharZero R<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hΦ₂ : Submodule.span R Φ = ⊤<VAR>f g : Module.Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : Set.MapsTo (⇑(Module.preReflection x g)) Φ Φ<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>CharZero R<VAR>NoZeroSMulDivisors R M<VAR>x : M<VAR>hx : x ≠ 0<VAR>Φ : Set M<VAR>hΦ₁ : Φ.Finite<VAR>hx' : x ∈ Submodule.span R Φ<VAR>f g : Module.Dual R M<VAR>hf₁ : f x = 2<VAR>hf₂ : Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ<VAR>hg₁ : g x = 2<VAR>hg₂ : Set.MapsTo (⇑(Module.preReflection x g)) Φ Φ<GOAL>(Submodule.span R Φ).subtype.dualMap f = (Submodule.span R Φ).subtype.dualMap g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>f : Module.Dual R M<VAR>y : M<VAR>g : Module.Dual R M<VAR>NoZeroSMulDivisors ℤ M<VAR>Φ : Set M<VAR>hΦ : Φ.Finite<VAR>hfx : f x = 2<VAR>hgy : g y = 2<VAR>hgx : g x = 2<VAR>hfy : f y = 2<VAR>hxfΦ : Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ<VAR>hygΦ : Set.MapsTo (⇑(Module.preReflection y g)) Φ Φ<VAR>hyΦ : y ∈ Φ<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u_3<VAR>NoZeroSMulDivisors ℤ M<VAR>r : ι ↪ M<VAR>c : ι → Module.Dual R M<VAR>hfin : (Set.range ⇑r).Finite<VAR>h_two : ∀ (i : ι), (c i) (r i) = 2<VAR>h_mapsTo : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (r i) (c i))) (Set.range ⇑r) (Set.range ⇑r)<GOAL>Set.InjOn (⇑(Submodule.span R (Set.range ⇑r)).subtype.dualMap) (Set.range c)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N<VAR>h : ∀ (i : ι) (x : M i), φ (DFinsupp.single i x) = ψ (DFinsupp.single i x)<GOAL>φ = ψ
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N<VAR>h : ∀ (i : ι), φ ∘ₗ DFinsupp.lsingle i = ψ ∘ₗ DFinsupp.lsingle i<GOAL>φ = ψ
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : ι → Type u_4<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>DecidableEq ι<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → M ↑i<GOAL>(DFinsupp.lmk s) x = DFinsupp.mk s x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : ι → Type u_4<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>DecidableEq ι<VAR>i : ι<VAR>x : M i<GOAL>(DFinsupp.lsingle i) x = DFinsupp.single i x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : ι → Type u_4<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>i : ι<VAR>f : Π₀ (i : ι), M i<GOAL>(DFinsupp.lapply i) f = f i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>F : (i : ι) → M i →ₗ[R] N<VAR>a : Π₀ (i : ι), M i<GOAL>((DFinsupp.lsum S) F) a = (DFinsupp.sumAddHom fun i => (F i).toAddMonoidHom) a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>F : (Π₀ (i : ι), M i) →ₗ[R] N<VAR>i : ι<GOAL>(DFinsupp.lsum S).symm F i = F ∘ₗ DFinsupp.lsingle i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>Semiring S<VAR>Module S N<VAR>SMulCommClass R S N<VAR>F : (i : ι) → M i →ₗ[R] N<VAR>i : ι<VAR>x : M i<GOAL>((DFinsupp.lsum S) F) (DFinsupp.single i x) = (F i) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>(i : ι) → AddCommMonoid (β₁ i)<VAR>(i : ι) → AddCommMonoid (β₂ i)<VAR>(i : ι) → Module R (β₁ i)<VAR>(i : ι) → Module R (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i<VAR>hf : ∀ (i : ι), f i 0 = 0<VAR>r : R<VAR>hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x<VAR>g : Π₀ (i : ι), β₁ i<GOAL>DFinsupp.mapRange f hf (r • g) = r • DFinsupp.mapRange f hf g
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>(i : ι) → AddCommMonoid (β₁ i)<VAR>(i : ι) → AddCommMonoid (β₂ i)<VAR>(i : ι) → Module R (β₁ i)<VAR>(i : ι) → Module R (β₂ i)<VAR>f : (i : ι) → β₁ i →ₗ[R] β₂ i<VAR>x : Π₀ (i : ι), β₁ i<GOAL>(DFinsupp.mapRange.linearMap f) x = DFinsupp.mapRange (fun i x => (f i) x) ⋯ x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>β₂ : ι → Type u_8<VAR>(i : ι) → AddCommMonoid (β₂ i)<VAR>(i : ι) → Module R (β₂ i)<GOAL>(DFinsupp.mapRange.linearMap fun i => LinearMap.id) = LinearMap.id
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>β : ι → Type u_6<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → AddCommMonoid (β₁ i)<VAR>(i : ι) → AddCommMonoid (β₂ i)<VAR>(i : ι) → Module R (β i)<VAR>(i : ι) → Module R (β₁ i)<VAR>(i : ι) → Module R (β₂ i)<VAR>f : (i : ι) → β₁ i →ₗ[R] β₂ i<VAR>f₂ : (i : ι) → β i →ₗ[R] β₁ i<GOAL>(DFinsupp.mapRange.linearMap fun i => f i ∘ₗ f₂ i) = DFinsupp.mapRange.linearMap f ∘ₗ DFinsupp.mapRange.linearMap f₂
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>(i : ι) → AddCommMonoid (β₁ i)<VAR>(i : ι) → AddCommMonoid (β₂ i)<VAR>(i : ι) → Module R (β₁ i)<VAR>(i : ι) → Module R (β₂ i)<VAR>DecidableEq ι<VAR>f : (i : ι) → β₁ i →ₗ[R] β₂ i<VAR>h : (i : ι) → β₂ i →ₗ[R] N<VAR>l : Π₀ (i : ι), β₁ i<GOAL>((DFinsupp.lsum ℕ) h) ((DFinsupp.mapRange.linearMap f) l) = ((DFinsupp.lsum ℕ) fun i => h i ∘ₗ f i) l
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>(i : ι) → AddCommMonoid (β₁ i)<VAR>(i : ι) → AddCommMonoid (β₂ i)<VAR>(i : ι) → Module R (β₁ i)<VAR>(i : ι) → Module R (β₂ i)<VAR>e : (i : ι) → β₁ i ≃ₗ[R] β₂ i<VAR>x : Π₀ (i : ι), β₁ i<GOAL>(DFinsupp.mapRange.linearEquiv e) x = DFinsupp.mapRange (fun i x => (e i) x) ⋯ x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>β₁ : ι → Type u_7<VAR>(i : ι) → AddCommMonoid (β₁ i)<VAR>(i : ι) → Module R (β₁ i)<GOAL>(DFinsupp.mapRange.linearEquiv fun i => LinearEquiv.refl R (β₁ i)) = LinearEquiv.refl R (Π₀ (i : ι), β₁ i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>β : ι → Type u_6<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>(i : ι) → AddCommMonoid (β i)<VAR>(i : ι) → AddCommMonoid (β₁ i)<VAR>(i : ι) → AddCommMonoid (β₂ i)<VAR>(i : ι) → Module R (β i)<VAR>(i : ι) → Module R (β₁ i)<VAR>(i : ι) → Module R (β₂ i)<VAR>f : (i : ι) → β i ≃ₗ[R] β₁ i<VAR>f₂ : (i : ι) → β₁ i ≃ₗ[R] β₂ i<GOAL>(DFinsupp.mapRange.linearEquiv fun i => f i ≪≫ₗ f₂ i) = DFinsupp.mapRange.linearEquiv f ≪≫ₗ DFinsupp.mapRange.linearEquiv f₂
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>β₁ : ι → Type u_7<VAR>β₂ : ι → Type u_8<VAR>(i : ι) → AddCommMonoid (β₁ i)<VAR>(i : ι) → AddCommMonoid (β₂ i)<VAR>(i : ι) → Module R (β₁ i)<VAR>(i : ι) → Module R (β₂ i)<VAR>e : (i : ι) → β₁ i ≃ₗ[R] β₂ i<GOAL>(DFinsupp.mapRange.linearEquiv e).symm = DFinsupp.mapRange.linearEquiv fun i => (e i).symm
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>(x : N) → Decidable (x ≠ 0)<VAR>f : (i : ι) → M i →ₗ[R] N<VAR>x : Π₀ (i : ι), M i<GOAL>(DFinsupp.coprodMap f) x = (DFinsupp.mapRange (fun i => ⇑(f i)) ⋯ x).sum fun x => id
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : ι → Type u_4<VAR>N : Type u_5<VAR>Semiring R<VAR>(i : ι) → AddCommMonoid (M i)<VAR>(i : ι) → Module R (M i)<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>f : (i : ι) → M i →ₗ[R] N<VAR>i : ι<VAR>x : M i<GOAL>(DFinsupp.coprodMap f) (DFinsupp.single i x) = (f i) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>β : ι → Type u_6<VAR>(i : ι) → Zero (β i)<VAR>(i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>S : Submodule R N<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i → N<VAR>h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ S<GOAL>f.sum g ∈ S
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>β : ι → Type u_6<VAR>(i : ι) → AddZeroClass (β i)<VAR>S : Submodule R N<VAR>f : Π₀ (i : ι), β i<VAR>g : (i : ι) → β i →+ N<VAR>h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ S<GOAL>(DFinsupp.sumAddHom g) f ∈ S
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>p : ι → Submodule R N<GOAL>iSup p = LinearMap.range ((DFinsupp.lsum ℕ) fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>S : ι → Submodule R N<GOAL>⨆ i, ⨆ (_ : p i), S i = LinearMap.range (((DFinsupp.lsum ℕ) fun i => (S i).subtype) ∘ₗ DFinsupp.filterLinearMap R (fun i => ↥(S i)) p)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>p : ι → Submodule R N<VAR>x : N<GOAL>x ∈ iSup p ↔ ∃ f, ((DFinsupp.lsum ℕ) fun i => (p i).subtype) f = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>p : ι → Submodule R N<VAR>(i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)<VAR>x : N<GOAL>x ∈ iSup p ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>DecidableEq ι<VAR>p : ι → Prop<VAR>DecidablePred p<VAR>S : ι → Submodule R N<VAR>x : N<GOAL>x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ f, ((DFinsupp.lsum ℕ) fun i => (S i).subtype) (DFinsupp.filter p f) = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>p : ι → Submodule R N<VAR>x : N<GOAL>x ∈ iSup p ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi => xi) = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>s : Finset ι<VAR>p : ι → Submodule R N<VAR>a : N<GOAL>a ∈ ⨆ i ∈ s, p i ↔ ∃ μ, ∑ i ∈ s, ↑(μ i) = a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>p : ι → Submodule R N<GOAL>CompleteLattice.Independent p ↔ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((DFinsupp.lsum ℕ) fun i => (p i).subtype) (DFinsupp.erase i v) = ↑x → x = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>p : ι → Submodule R N<VAR>h : Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)<GOAL>CompleteLattice.Independent p
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>AddCommMonoid N<VAR>p : ι → AddSubmonoid N<VAR>h : Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)<GOAL>CompleteLattice.Independent p
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>(m : R) → Decidable (m ≠ 0)<VAR>p : ι → Submodule R N<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<GOAL>((DFinsupp.lsum ℕ) fun i => (p i).subtype) ∘ₗ (DFinsupp.mapRange.linearMap fun i => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R) = Finsupp.total ι N R v
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>AddCommGroup N<VAR>p : ι → AddSubgroup N<VAR>h : Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)<GOAL>CompleteLattice.Independent p
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>Ring R<VAR>AddCommGroup N<VAR>Module R N<VAR>p : ι → Submodule R N<VAR>h : CompleteLattice.Independent p<GOAL>Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>AddCommGroup N<VAR>p : ι → AddSubgroup N<VAR>h : CompleteLattice.Independent p<GOAL>Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>Ring R<VAR>AddCommGroup N<VAR>Module R N<VAR>p : ι → Submodule R N<GOAL>CompleteLattice.Independent p ↔ Function.Injective ⇑((DFinsupp.lsum ℕ) fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>DecidableEq ι<VAR>AddCommGroup N<VAR>p : ι → AddSubgroup N<GOAL>CompleteLattice.Independent p ↔ Function.Injective ⇑(DFinsupp.sumAddHom fun i => (p i).subtype)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Ring R<VAR>AddCommGroup N<VAR>Module R N<VAR>NoZeroSMulDivisors R N<VAR>p : ι → Submodule R N<VAR>hp : CompleteLattice.Independent p<VAR>v : ι → N<VAR>hv : ∀ (i : ι), v i ∈ p i<VAR>hv' : ∀ (i : ι), v i ≠ 0<GOAL>LinearIndependent R v
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>N : Type u_5<VAR>Ring R<VAR>AddCommGroup N<VAR>Module R N<VAR>NoZeroSMulDivisors R N<VAR>v : ι → N<VAR>h_ne_zero : ∀ (i : ι), v i ≠ 0<GOAL>(CompleteLattice.Independent fun i => Submodule.span R {v i}) ↔ LinearIndependent R v
<VAR>R : Type u_6<VAR>R₂ : Type u_8<VAR>M : Type u_14<VAR>M₂ : Type u_17<VAR>ι : Type u_22<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>γ : ι → Type u_25<VAR>DecidableEq ι<VAR>(i : ι) → Zero (γ i)<VAR>(i : ι) → (x : γ i) → Decidable (x ≠ 0)<VAR>t : Π₀ (i : ι), γ i<VAR>g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂<GOAL>⇑(t.sum g) = ⇑(t.sum fun i d => g i d)
<VAR>R : Type u_6<VAR>R₂ : Type u_8<VAR>M : Type u_14<VAR>M₂ : Type u_17<VAR>ι : Type u_22<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>γ : ι → Type u_25<VAR>DecidableEq ι<VAR>(i : ι) → Zero (γ i)<VAR>(i : ι) → (x : γ i) → Decidable (x ≠ 0)<VAR>t : Π₀ (i : ι), γ i<VAR>g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂<VAR>b : M<GOAL>(t.sum g) b = t.sum fun i d => (g i d) b
<VAR>R : Type u_6<VAR>R₂ : Type u_8<VAR>M : Type u_14<VAR>M₂ : Type u_17<VAR>ι : Type u_22<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>γ : ι → Type u_25<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (γ i)<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>t : Π₀ (i : ι), γ i<VAR>g : (i : ι) → γ i →+ M<GOAL>f ((DFinsupp.sumAddHom g) t) = (DFinsupp.sumAddHom fun i => f.toAddMonoidHom.comp (g i)) t
<VAR>R : Type u_6<VAR>R₂ : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_9<VAR>ι : Type u_10<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₁ : R₂ →+* R<VAR>RingHomInvPair τ₁₂ τ₂₁<VAR>RingHomInvPair τ₂₁ τ₁₂<VAR>γ : ι → Type u_11<VAR>DecidableEq ι<VAR>(i : ι) → AddZeroClass (γ i)<VAR>f : M ≃ₛₗ[τ₁₂] M₂<VAR>t : Π₀ (i : ι), γ i<VAR>g : (i : ι) → γ i →+ M<GOAL>f ((DFinsupp.sumAddHom g) t) = (DFinsupp.sumAddHom fun i => f.toAddEquiv.toAddMonoidHom.comp (g i)) t
<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>self : S.IsPrincipal<GOAL>∃ a, S = Submodule.span R {a}
<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<GOAL>S.IsPrincipal ↔ ∃ a, S = Submodule.span R {a}
<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>S.IsPrincipal<GOAL>∃ a, S = Submodule.span R {a}
<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>x ∈ Submodule.span R s ↔ ∀ (p : Submodule R M), s ⊆ ↑p → x ∈ 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>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<VAR>p : Submodule R M<GOAL>Submodule.span R s ≤ p ↔ s ⊆ ↑p
<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<VAR>h : s ⊆ t<GOAL>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<GOAL>Monotone (Submodule.span R)
<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<VAR>h₁ : s ⊆ ↑p<VAR>h₂ : p ≤ Submodule.span R s<GOAL>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>p : Submodule R M<GOAL>Submodule.span R ↑p = p
<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<VAR>hs : s ⊆ ↑(Submodule.span R t)<VAR>ht : t ⊆ ↑(Submodule.span R s)<GOAL>Submodule.span R s = Submodule.span R t
<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>SetLike S M<VAR>AddSubmonoidClass S M<VAR>SMulMemClass S R M<VAR>s : S<GOAL>↑(Submodule.span R ↑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>p : Submodule R M<VAR>Semiring S<VAR>SMul S R<VAR>Module S M<VAR>IsScalarTower S R M<GOAL>Submodule.span S ↑p = Submodule.restrictScalars S 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>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>f : F<VAR>s : Set M<VAR>N : Submodule R₂ M₂<GOAL>⇑f '' ↑(Submodule.span R s) ⊆ ↑N ↔ ∀ m ∈ s, f m ∈ N
<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>f : F<VAR>s : Set M<GOAL>⇑f '' ↑(Submodule.span R s) ⊆ ↑(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>s : Set M<GOAL>Submodule.map f (Submodule.span R s) = 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>s : Set M<VAR>N : Submodule R₂ M₂<GOAL>Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f 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<GOAL>Submodule.span R (insert 0 s) = 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>f : F<VAR>s : Set M₂<GOAL>Submodule.span R (⇑f ⁻¹' s) ≤ Submodule.comap f (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>↑(AddSubmonoid.closure 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>AddSubmonoid.closure s ≤ (Submodule.span R s).toAddSubmonoid
<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 ↑(AddSubmonoid.closure 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>p : M → Prop<VAR>h : x ∈ Submodule.span R s<VAR>mem : ∀ x ∈ s, p x<VAR>zero : p 0<VAR>add : ∀ (x y : M), p x → p y → p (x + y)<VAR>smul : ∀ (a : R) (x : M), p x → p (a • 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 : M → M → Prop<VAR>a b : M<VAR>ha : a ∈ Submodule.span R s<VAR>hb : b ∈ Submodule.span R s<VAR>mem_mem : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>zero_left : ∀ (y : M), p 0 y<VAR>zero_right : ∀ (x : M), p x 0<VAR>add_left : ∀ (x₁ x₂ y : M), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>add_right : ∀ (x y₁ y₂ : M), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>smul_left : ∀ (r : R) (x y : M), p x y → p (r • x) y<VAR>smul_right : ∀ (r : R) (x y : M), p x y → p x (r • y)<GOAL>p a b