ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>h : F.Stable<GOAL>∃ n₀, ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>h : F.Stable<GOAL>∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<GOAL>F.Stable ↔ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>e : F.N 0 ≤ F'.N 0<GOAL>∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>h' : F'.Stable<VAR>e : F.N 0 = F'.N 0<GOAL>∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>f : PolynomialModule R M<GOAL>f ∈ F.submodule ↔ ∀ (i : ℕ), f i ∈ F.N i
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<GOAL>(F ⊓ F').submodule = F.submodule ⊓ F'.submodule
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<GOAL>AddSubmonoid.closure (⋃ i, ⇑(PolynomialModule.single R i) '' ↑(F.N i)) = F.submodule.toAddSubmonoid
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<GOAL>Submodule.span (↥(reesAlgebra I)) (⋃ i, ⇑(PolynomialModule.single R i) '' ↑(F.N i)) = F.submodule
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>n₀ : ℕ<GOAL>F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(PolynomialModule.single R i) '' ↑(F.N i)) ↔ ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>hF' : ∀ (i : ℕ), (F.N i).FG<GOAL>F.submodule.FG ↔ F.Stable
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>IsNoetherianRing R<VAR>Module.Finite R M<VAR>hF : F.Stable<VAR>F' : I.Filtration M<VAR>hf : F' ≤ F<GOAL>F'.Stable
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>F' : I.Filtration M<VAR>IsNoetherianRing R<VAR>Module.Finite R M<VAR>hF : F.Stable<GOAL>(F ⊓ F').Stable
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>F' : I.Filtration M<VAR>IsNoetherianRing R<VAR>Module.Finite R M<VAR>hF : F.Stable<GOAL>(F' ⊓ F).Stable
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>IsNoetherianRing R<VAR>Module.Finite R M<VAR>N : Submodule R M<GOAL>∃ k, ∀ n ≥ k, I ^ n • ⊤ ⊓ N = I ^ (n - k) • (I ^ k • ⊤ ⊓ N)
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>IsNoetherianRing R<VAR>Module.Finite R M<VAR>x : M<GOAL>x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>IsNoetherianRing R<VAR>LocalRing R<VAR>Module.Finite R M<VAR>h : I ≠ ⊤<GOAL>⨅ i, I ^ i • ⊤ = ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>IsNoetherianRing R<VAR>LocalRing R<VAR>h : I ≠ ⊤<GOAL>⨅ i, I ^ i = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsNoetherianRing R<VAR>LocalRing R<VAR>I : Ideal R<GOAL>IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>IsNoetherianRing R<VAR>IsDomain R<VAR>h : I ≠ ⊤<GOAL>⨅ i, I ^ i = ⊥
<VAR>R : Type u_1<VAR>Semiring R<GOAL>Ideal.ofList [] = ⊥
<VAR>R : Type u_1<VAR>Semiring R<VAR>rs₁ rs₂ : List R<GOAL>Ideal.ofList (rs₁ ++ rs₂) = Ideal.ofList rs₁ ⊔ Ideal.ofList rs₂
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>Ideal.ofList [r] = Ideal.span {r}
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<VAR>rs : List R<GOAL>Ideal.ofList (r :: rs) = Ideal.span {r} ⊔ Ideal.ofList rs
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>rs : List R<GOAL>Ideal.map f (Ideal.ofList rs) = Ideal.ofList (List.map (⇑f) rs)
<VAR>R : Type u_7<VAR>CommSemiring R<VAR>r : R<VAR>rs : List R<VAR>M : Type u_8<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>Ideal.ofList (r :: rs) • N = r • N ⊔ Ideal.ofList rs • N
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>I : Ideal R<VAR>f : M →ₗ[R] M₂<GOAL>I • ⊤ ≤ Submodule.comap f (I • ⊤)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>r : R<VAR>rs : List R<VAR>f : M →ₗ[R] M₂<GOAL>↑(Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M₂ r rs) ∘ₗ (Ideal.ofList (r :: rs) • ⊤).mapQ (Ideal.ofList (r :: rs) • ⊤) f ⋯ = (Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) ((QuotSMulTop.map r) f) ⋯ ∘ₗ ↑(Submodule.quotOfListConsSMulTopEquivQuotSMulTopInner M r rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<GOAL>⊤ = Ideal.ofList (r :: rs) • ⊤ ↔ ⊤ = Ideal.ofList rs • ⊤
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<VAR>self : RingTheory.Sequence.IsWeaklyRegular M rs<VAR>i : ℕ<VAR>h : i < rs.length<GOAL>IsSMulRegular (M ⧸ Ideal.ofList (List.take i rs) • ⊤) rs[i]
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M rs ↔ ∀ (i : ℕ) (h : i < rs.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take i rs) • ⊤) rs[i]
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M rs ↔ ∀ (i : Fin rs.length), IsSMulRegular (M ⧸ Ideal.ofList (List.take (↑i) rs) • ⊤) (rs.get i)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<VAR>self : RingTheory.Sequence.IsRegular M rs<GOAL>⊤ ≠ Ideal.ofList rs • ⊤
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<GOAL>RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M rs ∧ ⊤ ≠ Ideal.ofList rs • ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module S M₂<VAR>f : M →+ M₂<VAR>as : List R<VAR>bs : List S<VAR>hf : Function.Surjective ⇑f<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), f (r • x) = s • f x) as bs<GOAL>AddSubgroup.map f (Ideal.ofList as • ⊤).toAddSubgroup = (Ideal.ofList bs • ⊤).toAddSubgroup
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module S M₂<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<GOAL>RingTheory.Sequence.IsWeaklyRegular M as ↔ RingTheory.Sequence.IsWeaklyRegular M₂ bs
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>rs : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M₂ (List.map (⇑σ) rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃ₗ[R] M₂<VAR>rs : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M₂ rs
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module S M₂<VAR>e : M ≃+ M₂<VAR>as : List R<VAR>bs : List S<VAR>h : List.Forall₂ (fun r s => ∀ (x : M), e (r • x) = s • e x) as bs<GOAL>RingTheory.Sequence.IsRegular M as ↔ RingTheory.Sequence.IsRegular M₂ bs
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>rs : List R<GOAL>RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsRegular M₂ (List.map (⇑σ) rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>e : M ≃ₗ[R] M₂<VAR>rs : List R<GOAL>RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsRegular M₂ rs
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>rs : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M (List.map (⇑(algebraMap R S)) rs) ↔ RingTheory.Sequence.IsWeaklyRegular M rs
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<GOAL>RingTheory.Sequence.IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.IsRegular (QuotSMulTop r M) rs
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<GOAL>RingTheory.Sequence.IsRegular M (r :: rs) ↔ IsSMulRegular M r ∧ RingTheory.Sequence.IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>RingTheory.Sequence.IsWeaklyRegular M []
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<VAR>h1 : IsSMulRegular M r<VAR>h2 : RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs<GOAL>RingTheory.Sequence.IsWeaklyRegular M (r :: rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<VAR>h1 : IsSMulRegular M r<VAR>h2 : RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)<GOAL>RingTheory.Sequence.IsWeaklyRegular M (r :: rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>RingTheory.Sequence.IsWeaklyRegular M [r] ↔ IsSMulRegular M r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs₁ rs₂ : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M (rs₁ ++ rs₂) ↔ RingTheory.Sequence.IsWeaklyRegular M rs₁ ∧ RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) rs₂
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs₁ rs₂ : List R<GOAL>RingTheory.Sequence.IsWeaklyRegular M (rs₁ ++ rs₂) ↔ RingTheory.Sequence.IsWeaklyRegular M rs₁ ∧ RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₁ • ⊤) (List.map (⇑(Ideal.Quotient.mk (Ideal.ofList rs₁))) rs₂)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial M<GOAL>RingTheory.Sequence.IsRegular M []
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<VAR>h1 : IsSMulRegular M r<VAR>h2 : RingTheory.Sequence.IsRegular (QuotSMulTop r M) rs<GOAL>RingTheory.Sequence.IsRegular M (r :: rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>rs : List R<VAR>h1 : IsSMulRegular M r<VAR>h2 : RingTheory.Sequence.IsRegular (QuotSMulTop r M) (List.map (⇑(Ideal.Quotient.mk (Ideal.span {r}))) rs)<GOAL>RingTheory.Sequence.IsRegular M (r :: rs)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<VAR>h : RingTheory.Sequence.IsRegular M rs<VAR>N : Submodule R M<GOAL>Nontrivial (M ⧸ Ideal.ofList rs • N)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<VAR>h : RingTheory.Sequence.IsRegular M rs<GOAL>Nontrivial M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial M<VAR>Module.Finite R M<VAR>rs : List R<VAR>h : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson<GOAL>RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M rs
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>LocalRing R<VAR>Nontrivial M<VAR>Module.Finite R M<VAR>rs : List R<VAR>h : ∀ r ∈ rs, r ∈ LocalRing.maximalIdeal R<GOAL>RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M rs
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>rs : List R<GOAL>RingTheory.Sequence.IsRegular M rs → rs = []
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module.Flat R M₂<VAR>rs : List R<VAR>h : RingTheory.Sequence.IsWeaklyRegular M rs<GOAL>RingTheory.Sequence.IsWeaklyRegular (TensorProduct R M₂ M) rs
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>Module R M<VAR>Module R M₂<VAR>Module.Flat R M₂<VAR>rs : List R<VAR>h : RingTheory.Sequence.IsWeaklyRegular M rs<GOAL>RingTheory.Sequence.IsWeaklyRegular (TensorProduct R M M₂) rs
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M₂ : Type u_4<VAR>M₃ : Type u_5<VAR>M₄ : Type u_6<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup M₂<VAR>AddCommGroup M₃<VAR>AddCommGroup M₄<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>Module R M₄<VAR>rs : List R<VAR>f₁ : M →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>f₃ : M₃ →ₗ[R] M₄<VAR>h₁₂ : Function.Exact ⇑f₁ ⇑f₂<VAR>h₂₃ : Function.Exact ⇑f₂ ⇑f₃<VAR>h₃ : Function.Surjective ⇑f₃<VAR>h₄ : RingTheory.Sequence.IsWeaklyRegular M₄ rs<GOAL>Function.Exact ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₁ ⋯) ⇑((Ideal.ofList rs • ⊤).mapQ (Ideal.ofList rs • ⊤) f₂ ⋯)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>a b : R<VAR>h1 : RingTheory.Sequence.IsWeaklyRegular M [a, b]<VAR>h2 : Submodule.torsionBy R M b = a • Submodule.torsionBy R M b → Submodule.torsionBy R M b = ⊥<GOAL>RingTheory.Sequence.IsWeaklyRegular M [b, a]
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<VAR>h' : ∀ (a b : R) (rs' : List R), (a :: b :: rs').Subperm rs → let K := Submodule.torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b; K = a • K → K = ⊥<VAR>rs₁ rs₂ : List R<VAR>rs₀ : List R<VAR>h₁₂ : rs₁.Perm rs₂<VAR>H₁ : (rs₀ ++ rs₁).Subperm rs<VAR>H₃ : (rs₀ ++ rs₂).Subperm rs<VAR>h : RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₁<GOAL>RingTheory.Sequence.IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) rs₂
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>rs : List R<VAR>h : RingTheory.Sequence.IsWeaklyRegular M rs<VAR>rs' : List R<VAR>h'' : rs.Perm rs'<VAR>h' : ∀ (a b : R) (rs' : List R), (a :: b :: rs').Subperm rs → let K := Submodule.torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b; K = a • K → K = ⊥<GOAL>RingTheory.Sequence.IsWeaklyRegular M rs'
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>rs rs' : List R<VAR>h1 : RingTheory.Sequence.IsWeaklyRegular M rs<VAR>h2 : rs.Perm rs'<VAR>h3 : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson<GOAL>RingTheory.Sequence.IsWeaklyRegular M rs'
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>rs rs' : List R<VAR>h1 : RingTheory.Sequence.IsRegular M rs<VAR>h2 : rs.Perm rs'<VAR>h3 : ∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson<GOAL>RingTheory.Sequence.IsRegular M rs'
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>LocalRing R<VAR>IsNoetherian R M<VAR>rs rs' : List R<VAR>h1 : RingTheory.Sequence.IsWeaklyRegular M rs<VAR>h2 : rs.Perm rs'<VAR>h3 : ∀ r ∈ rs, r ∈ LocalRing.maximalIdeal R<GOAL>RingTheory.Sequence.IsWeaklyRegular M rs'
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>LocalRing R<VAR>IsNoetherian R M<VAR>rs rs' : List R<VAR>h1 : RingTheory.Sequence.IsRegular M rs<VAR>h2 : rs.Perm rs'<GOAL>RingTheory.Sequence.IsRegular M rs'
<VAR>R : Type u_1<VAR>Ring R<VAR>Fintype R<VAR>DecidableEq R<VAR>h : Fintype.card R ≤ 2<GOAL>Finset.univ = {0, 1}
<VAR>R : Type u_1<VAR>Ring R<VAR>Fintype R<VAR>DecidableEq R<VAR>h : Fintype.card R ≤ 3<GOAL>Finset.univ = {0, 1, -1}
<VAR>M₀ : Type u_2<VAR>MonoidWithZero M₀<VAR>Nontrivial M₀<VAR>Fintype M₀<GOAL>Fintype.card M₀ˣ < Fintype.card M₀
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>CommSemiring Rₛ<VAR>Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>Module Rₛ M'<VAR>IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>v : Set M<VAR>hv : Submodule.span R v = ⊤<GOAL>Submodule.span Rₛ (⇑f '' v) = ⊤
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>CommSemiring Rₛ<VAR>Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>Module Rₛ M'<VAR>IsScalarTower R Rₛ M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<VAR>ι : Type u_5<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>LinearIndependent Rₛ (⇑f ∘ v)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>CommSemiring Rₛ<VAR>Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module Rₛ M<VAR>IsScalarTower R Rₛ M<VAR>ι : Type u_5<VAR>b : ι → M<VAR>hli : LinearIndependent R b<GOAL>LinearIndependent Rₛ b
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>CommRing Rₛ<VAR>Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>Mₛ : Type u_4<VAR>AddCommGroup M<VAR>AddCommGroup Mₛ<VAR>Module R M<VAR>Module R Mₛ<VAR>Module Rₛ Mₛ<VAR>f : M →ₗ[R] Mₛ<VAR>IsLocalizedModule S f<VAR>IsScalarTower R Rₛ Mₛ<VAR>ι : Type u_5<VAR>b : Basis ι R M<VAR>i : ι<GOAL>(Basis.ofIsLocalizedModule Rₛ S f b) i = f (b i)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>CommRing Rₛ<VAR>Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>Mₛ : Type u_4<VAR>AddCommGroup M<VAR>AddCommGroup Mₛ<VAR>Module R M<VAR>Module R Mₛ<VAR>Module Rₛ Mₛ<VAR>f : M →ₗ[R] Mₛ<VAR>IsLocalizedModule S f<VAR>IsScalarTower R Rₛ Mₛ<VAR>ι : Type u_5<VAR>b : Basis ι R M<VAR>m : M<VAR>i : ι<GOAL>((Basis.ofIsLocalizedModule Rₛ S f b).repr (f m)) i = (algebraMap R Rₛ) ((b.repr m) i)
<VAR>R : Type u_1<VAR>Rₛ : Type u_2<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>CommRing Rₛ<VAR>Algebra R Rₛ<VAR>hT : IsLocalization S Rₛ<VAR>M : Type u_3<VAR>Mₛ : Type u_4<VAR>AddCommGroup M<VAR>AddCommGroup Mₛ<VAR>Module R M<VAR>Module R Mₛ<VAR>Module Rₛ Mₛ<VAR>f : M →ₗ[R] Mₛ<VAR>IsLocalizedModule S f<VAR>IsScalarTower R Rₛ Mₛ<VAR>ι : Type u_5<VAR>b : Basis ι R M<GOAL>Submodule.span R (Set.range ⇑(Basis.ofIsLocalizedModule Rₛ S f b)) = LinearMap.range f
<VAR>R : Type u_3<VAR>Rₛ : Type u_4<VAR>CommSemiring R<VAR>CommRing Rₛ<VAR>Algebra R Rₛ<VAR>S : Submonoid R<VAR>hT : IsLocalization S Rₛ<VAR>A : Type u_5<VAR>CommRing A<VAR>Algebra R A<VAR>Aₛ : Type u_6<VAR>CommRing Aₛ<VAR>Algebra A Aₛ<VAR>Algebra Rₛ Aₛ<VAR>Algebra R Aₛ<VAR>IsScalarTower R Rₛ Aₛ<VAR>IsScalarTower R A Aₛ<VAR>hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ<VAR>ι : Type u_7<VAR>v : ι → A<VAR>hv : LinearIndependent R v<GOAL>LinearIndependent Rₛ (⇑(algebraMap A Aₛ) ∘ v)
<VAR>R : Type u_3<VAR>Rₛ : Type u_4<VAR>CommSemiring R<VAR>CommRing Rₛ<VAR>Algebra R Rₛ<VAR>S : Submonoid R<VAR>hT : IsLocalization S Rₛ<VAR>A : Type u_5<VAR>CommRing A<VAR>Algebra R A<VAR>Aₛ : Type u_6<VAR>CommRing Aₛ<VAR>Algebra A Aₛ<VAR>Algebra Rₛ Aₛ<VAR>Algebra R Aₛ<VAR>IsScalarTower R Rₛ Aₛ<VAR>IsScalarTower R A Aₛ<VAR>hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ<VAR>v : Set A<VAR>hv : Submodule.span R v = ⊤<GOAL>Submodule.span Rₛ (⇑(algebraMap A Aₛ) '' v) = ⊤
<VAR>R : Type u_3<VAR>Rₛ : Type u_4<VAR>CommSemiring R<VAR>CommRing Rₛ<VAR>Algebra R Rₛ<VAR>S : Submonoid R<VAR>hT : IsLocalization S Rₛ<VAR>A : Type u_5<VAR>CommRing A<VAR>Algebra R A<VAR>Aₛ : Type u_6<VAR>CommRing Aₛ<VAR>Algebra A Aₛ<VAR>Algebra Rₛ Aₛ<VAR>Algebra R Aₛ<VAR>IsScalarTower R Rₛ Aₛ<VAR>IsScalarTower R A Aₛ<VAR>hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ<VAR>ι : Type u_7<VAR>b : Basis ι R A<VAR>i : ι<GOAL>(Basis.localizationLocalization Rₛ S Aₛ b) i = (algebraMap A Aₛ) (b i)
<VAR>R : Type u_3<VAR>Rₛ : Type u_4<VAR>CommSemiring R<VAR>CommRing Rₛ<VAR>Algebra R Rₛ<VAR>S : Submonoid R<VAR>hT : IsLocalization S Rₛ<VAR>A : Type u_5<VAR>CommRing A<VAR>Algebra R A<VAR>Aₛ : Type u_6<VAR>CommRing Aₛ<VAR>Algebra A Aₛ<VAR>Algebra Rₛ Aₛ<VAR>Algebra R Aₛ<VAR>IsScalarTower R Rₛ Aₛ<VAR>IsScalarTower R A Aₛ<VAR>hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ<VAR>ι : Type u_7<VAR>b : Basis ι R A<VAR>x : A<VAR>i : ι<GOAL>((Basis.localizationLocalization Rₛ S Aₛ b).repr ((algebraMap A Aₛ) x)) i = (algebraMap R Rₛ) ((b.repr x) i)
<VAR>R : Type u_3<VAR>Rₛ : Type u_4<VAR>CommSemiring R<VAR>CommRing Rₛ<VAR>Algebra R Rₛ<VAR>S : Submonoid R<VAR>hT : IsLocalization S Rₛ<VAR>A : Type u_5<VAR>CommRing A<VAR>Algebra R A<VAR>Aₛ : Type u_6<VAR>CommRing Aₛ<VAR>Algebra A Aₛ<VAR>Algebra Rₛ Aₛ<VAR>Algebra R Aₛ<VAR>IsScalarTower R Rₛ Aₛ<VAR>IsScalarTower R A Aₛ<VAR>hA : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ<VAR>ι : Type u_7<VAR>b : Basis ι R A<GOAL>Submodule.span R (Set.range ⇑(Basis.localizationLocalization Rₛ S Aₛ b)) = LinearMap.range (IsScalarTower.toAlgHom R A Aₛ)
<VAR>R : Type u_3<VAR>K : Type u_4<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>V : Type u_5<VAR>AddCommGroup V<VAR>Module R V<VAR>Module K V<VAR>IsScalarTower R K V<VAR>ι : Type u_6<VAR>b : ι → V<GOAL>LinearIndependent R b ↔ LinearIndependent K b
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_4<VAR>CommSemiring A<VAR>Algebra R A<VAR>IsLocalization S A<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module A N<VAR>IsScalarTower R A N<VAR>f : M →ₗ[R] N<GOAL>↑R (LinearMap.extendScalarsOfIsLocalization S A f) = f
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_4<VAR>CommSemiring A<VAR>Algebra R A<VAR>IsLocalization S A<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module A N<VAR>IsScalarTower R A N<VAR>f : M →ₗ[A] N<GOAL>LinearMap.extendScalarsOfIsLocalization S A (↑R f) = f
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_4<VAR>CommSemiring A<VAR>Algebra R A<VAR>IsLocalization S A<VAR>M : Type u_5<VAR>N : Type u_6<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>IsScalarTower R A M<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module A N<VAR>IsScalarTower R A N<VAR>f : M →ₗ[R] N<VAR>x : M<GOAL>(LinearMap.extendScalarsOfIsLocalization S A f) x = f x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>N : Submonoid S<VAR>x : R<GOAL>x ∈ IsLocalization.localizationLocalizationSubmodule M N ↔ ∃ y z, (algebraMap R S) x = ↑y * (algebraMap R S) ↑z