ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>pb : PowerBasis A S<GOAL>pb.minpolyGen = minpoly A pb.gen
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>pb : PowerBasis A S<GOAL>IsIntegral A pb.gen
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>Nontrivial A<VAR>pb : PowerBasis A S<GOAL>(minpoly A pb.gen).degree = ↑pb.dim
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>Nontrivial A<VAR>pb : PowerBasis A S<GOAL>(minpoly A pb.gen).natDegree = pb.dim
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>pb : PowerBasis A S<GOAL>(Algebra.leftMulMatrix pb.basis) pb.gen = Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval y) f
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) pb.gen = y
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0<VAR>x : A<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((algebraMap A S) x) = (algebraMap A S') x
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0<VAR>x x' : S<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) (x * x') = ((pb.basis.constr A) fun i => y ^ ↑i) x * ((pb.basis.constr A) fun i => y ^ ↑i) x'
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0<GOAL>(pb.lift y hy) pb.gen = y
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (Polynomial.aeval y) (minpoly A pb.gen) = 0<VAR>f : A[X]<GOAL>(pb.lift y hy) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval y) f
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : { y // (Polynomial.aeval y) (minpoly A pb.gen) = 0 }<GOAL>pb.liftEquiv.symm y = pb.lift ↑y ⋯
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>f : S →ₐ[A] S'<GOAL>↑(pb.liftEquiv f) = f pb.gen
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain B<VAR>Algebra A B<VAR>Algebra A S<VAR>pb : PowerBasis A S<GOAL>∀ (a : S →ₐ[A] B), ↑(pb.liftEquiv' a) = a pb.gen
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>CommRing A<VAR>CommRing B<VAR>IsDomain B<VAR>Algebra A B<VAR>Algebra A S<VAR>pb : PowerBasis A S<GOAL>∀ (a : { y // y ∈ (minpoly A pb.gen).aroots B }), ⇑(pb.liftEquiv'.symm a) = ⇑((pb.basis.constr A) fun i => ↑a ^ ↑i)
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0<VAR>h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0<VAR>a : S<GOAL>(pb.equivOfRoot pb' h₁ h₂) a = (pb.lift pb'.gen h₂) a
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0<VAR>h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0<VAR>f : A[X]<GOAL>(pb.equivOfRoot pb' h₁ h₂) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval pb'.gen) f
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0<VAR>h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0<GOAL>(pb.equivOfRoot pb' h₁ h₂) pb.gen = pb'.gen
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0<VAR>h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0<GOAL>(pb.equivOfRoot pb' h₁ h₂).symm = pb'.equivOfRoot pb h₂ h₁
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h : minpoly A pb.gen = minpoly A pb'.gen<VAR>a : S<GOAL>(pb.equivOfMinpoly pb' h) a = (pb.lift pb'.gen ⋯) a
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h : minpoly A pb.gen = minpoly A pb'.gen<VAR>f : A[X]<GOAL>(pb.equivOfMinpoly pb' h) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval pb'.gen) f
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h : minpoly A pb.gen = minpoly A pb'.gen<GOAL>(pb.equivOfMinpoly pb' h) pb.gen = pb'.gen
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>S' : Type u_7<VAR>Ring S'<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>pb' : PowerBasis A S'<VAR>h : minpoly A pb.gen = minpoly A pb'.gen<GOAL>(pb.equivOfMinpoly pb' h).symm = pb'.equivOfMinpoly pb ⋯
<VAR>S : Type u_2<VAR>Ring S<VAR>K : Type u_6<VAR>Field K<VAR>Algebra K S<VAR>x : S<GOAL>LinearIndependent K fun i => x ^ ↑i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>Nontrivial R<VAR>x y : S<VAR>hx : IsIntegral R x<VAR>hy : ∃ f, y = (Polynomial.aeval x) f<GOAL>y ∈ Submodule.span R (Set.range fun i => x ^ ↑i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>S' : Type u_7<VAR>CommRing S'<VAR>Algebra R S'<VAR>pb : PowerBasis R S<VAR>e : S ≃ₐ[R] S'<GOAL>(pb.map e).dim = pb.dim
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>S' : Type u_7<VAR>CommRing S'<VAR>Algebra R S'<VAR>pb : PowerBasis R S<VAR>e : S ≃ₐ[R] S'<GOAL>(pb.map e).gen = e pb.gen
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>S' : Type u_7<VAR>CommRing S'<VAR>Algebra R S'<VAR>pb : PowerBasis R S<VAR>e : S ≃ₐ[R] S'<GOAL>(pb.map e).basis = pb.basis.map e.toLinearEquiv
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>S' : Type u_7<VAR>CommRing S'<VAR>Algebra A S<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>e : S ≃ₐ[A] S'<GOAL>(pb.map e).minpolyGen = pb.minpolyGen
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>S' : Type u_7<VAR>CommRing S'<VAR>Algebra A S<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>e : S ≃ₐ[A] S'<VAR>h₁ : (Polynomial.aeval pb.gen) (minpoly A (pb.map e).gen) = 0<VAR>h₂ : (Polynomial.aeval (pb.map e).gen) (minpoly A pb.gen) = 0<GOAL>pb.equivOfRoot (pb.map e) h₁ h₂ = e
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>S' : Type u_7<VAR>CommRing S'<VAR>Algebra A S<VAR>Algebra A S'<VAR>pb : PowerBasis A S<VAR>e : S ≃ₐ[A] S'<VAR>h : minpoly A pb.gen = minpoly A (pb.map e).gen<GOAL>pb.equivOfMinpoly (pb.map e) h = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>B : PowerBasis R S<GOAL>Algebra.adjoin R {B.gen} = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>B : PowerBasis R S<VAR>x : S<VAR>hx : B.gen ∈ Algebra.adjoin R {x}<GOAL>Algebra.adjoin R {x} = ⊤
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hi : I.IsPrime<GOAL>I.IsPrimary
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hi : I.IsPrimary<GOAL>I.radical.IsPrime
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I J : Ideal R<VAR>hi : I.IsPrimary<VAR>hj : J.IsPrimary<VAR>hij : I.radical = J.radical<GOAL>(I ⊓ J).IsPrimary
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>self : IsArtinian R M<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>R : Type u_5<VAR>M : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>IsArtinian R M<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R P<VAR>f : M →ₗ[R] P<VAR>h : Function.Injective ⇑f<VAR>IsArtinian R P<GOAL>IsArtinian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>s t : Submodule R M<VAR>IsArtinian R ↥t<VAR>h : s ≤ t<GOAL>IsArtinian R ↥s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R P<VAR>f : M →ₗ[R] P<VAR>hf : Function.Surjective ⇑f<VAR>IsArtinian R M<GOAL>IsArtinian R P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R P<VAR>f : M ≃ₗ[R] P<VAR>IsArtinian R M<GOAL>IsArtinian R P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type u_4<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R P<VAR>Module R N<VAR>IsArtinian R M<VAR>IsArtinian R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hf : Function.Injective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>h : LinearMap.range f = LinearMap.ker g<GOAL>IsArtinian R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsArtinian R M ↔ WellFounded fun x x_1 => x < x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>Nontrivial R<VAR>IsArtinian R M<VAR>s : Set M<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>s.Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>(∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M') ↔ IsArtinian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>a : Set (Submodule R M)<VAR>ha : a.Nonempty<GOAL>∃ M' ∈ a, ∀ I ∈ a, ¬I < M'
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>(∀ (f : ℕ →o (Submodule R M)ᵒᵈ), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsArtinian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>f : ℕ →o (Submodule R M)ᵒᵈ<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → f n = f m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>f : ℕ →o (Submodule R M)ᵒᵈ<GOAL>Filter.EventuallyConst (⇑f) Filter.atTop
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>P : Submodule R M → Prop<VAR>hgt : ∀ (I : Submodule R M), (∀ J < I, P J) → P I<VAR>I : Submodule R M<GOAL>P I
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>f : M →ₗ[R] M<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, Codisjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>f : Module.End R M<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ⨅ m, LinearMap.range (f ^ m) = LinearMap.range (f ^ n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>IsNoetherian R M<VAR>f : M →ₗ[R] M<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, IsCompl (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>IsNoetherian R M<VAR>f : M →ₗ[R] M<GOAL>IsCompl (⨆ n, LinearMap.ker (f ^ n)) (⨅ n, LinearMap.range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>s : Function.Injective ⇑f<GOAL>Function.Surjective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>s : Function.Injective ⇑f<GOAL>Function.Bijective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>f : ℕ → Submodule R M<VAR>h : ∀ (n : ℕ), Disjoint ((partialSups (⇑OrderDual.toDual ∘ f)) n) (OrderDual.toDual (f (n + 1)))<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>r : R<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → LinearMap.range (r ^ n • LinearMap.id) = LinearMap.range (r ^ m • LinearMap.id)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinian R M<VAR>r : R<VAR>x : M<GOAL>∃ n y, r ^ n.succ • y = r ^ n • x
<VAR>R : Type u_1<VAR>Ring R<GOAL>IsArtinianRing R ↔ IsArtinian R R
<VAR>R : Type u_1<VAR>Ring R<VAR>h01 : 0 = 1<GOAL>IsArtinianRing R
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<GOAL>IsArtinian R M → IsArtinian R ↥N
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>Ring S<VAR>AddCommGroup M<VAR>Algebra R S<VAR>Module S M<VAR>Module R M<VAR>IsScalarTower R S M<VAR>h : IsArtinian R M<GOAL>IsArtinian S M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>IsArtinianRing R<VAR>hN : N.FG<GOAL>IsArtinian R ↥N
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>IsArtinianRing R<VAR>Module.Finite R S<GOAL>IsArtinianRing S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsArtinianRing R<VAR>A : Set M<VAR>hA : A.Finite<GOAL>IsArtinian R ↥(Submodule.span R A)
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Type u_2<VAR>Ring S<VAR>F : Type u_3<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>H : IsArtinianRing R<GOAL>IsArtinianRing S
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsArtinianRing R<GOAL>IsNilpotent ⊥.jacobson
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsArtinianRing R<VAR>S : Submonoid R<VAR>L : Type u_2<VAR>CommRing L<VAR>Algebra R L<VAR>IsLocalization S L<GOAL>Function.Surjective ⇑(algebraMap R L)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsArtinianRing R<VAR>S : Submonoid R<VAR>L : Type u_2<VAR>CommRing L<VAR>Algebra R L<VAR>IsLocalization S L<GOAL>IsArtinianRing L
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsArtinianRing R<VAR>p : Ideal R<GOAL>p.IsPrime ↔ p.IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsArtinianRing R<GOAL>{I | I.IsPrime}.Finite
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsArtinianRing R<GOAL>{I | I.IsMaximal}.Finite
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsArtinianRing R<GOAL>Finite ↑{I | I.IsMaximal}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsArtinianRing R<VAR>IsReduced R<GOAL>IsSemisimpleRing R
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>Ring R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>(⋃ n, (x ^ n).support).IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>self : HahnSeries.SummableFamily Γ R α<GOAL>(⋃ a, (self.toFun a).support).IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>self : HahnSeries.SummableFamily Γ R α<VAR>g : Γ<GOAL>{a | (self.toFun a).coeff g ≠ 0}.Finite
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>s : HahnSeries.SummableFamily Γ R α<GOAL>(⋃ a, (s a).support).IsPWO
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>s : HahnSeries.SummableFamily Γ R α<VAR>g : Γ<GOAL>(Function.support fun a => (s a).coeff g).Finite
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<GOAL>Function.Injective DFunLike.coe
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>s t : HahnSeries.SummableFamily Γ R α<VAR>h : ∀ (a : α), s a = t a<GOAL>s = t
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>s t : HahnSeries.SummableFamily Γ R α<GOAL>⇑(s + t) = ⇑s + ⇑t
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>s t : HahnSeries.SummableFamily Γ R α<VAR>a : α<GOAL>(s + t) a = s a + t a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<GOAL>⇑0 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>a : α<GOAL>0 a = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>s : HahnSeries.SummableFamily Γ R α<VAR>g : Γ<GOAL>s.hsum.coeff g = ∑ᶠ (i : α), (s i).coeff g
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>s : HahnSeries.SummableFamily Γ R α<GOAL>s.hsum.support ⊆ ⋃ a, (s a).support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>s t : HahnSeries.SummableFamily Γ R α<GOAL>(s + t).hsum = s.hsum + t.hsum
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommGroup R<VAR>α : Type u_3<VAR>s : HahnSeries.SummableFamily Γ R α<GOAL>⇑(-s) = -⇑s
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommGroup R<VAR>α : Type u_3<VAR>s : HahnSeries.SummableFamily Γ R α<VAR>a : α<GOAL>(-s) a = -s a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommGroup R<VAR>α : Type u_3<VAR>s t : HahnSeries.SummableFamily Γ R α<GOAL>⇑(s - t) = ⇑s - ⇑t
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommGroup R<VAR>α : Type u_3<VAR>s t : HahnSeries.SummableFamily Γ R α<VAR>a : α<GOAL>(s - t) a = s a - t a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>OrderedCancelAddCommMonoid Γ<VAR>Semiring R<VAR>α : Type u_3<VAR>x : HahnSeries Γ R<VAR>s : HahnSeries.SummableFamily Γ R α<VAR>a : α<GOAL>(x • s) a = x * s a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>OrderedCancelAddCommMonoid Γ<VAR>Semiring R<VAR>α : Type u_3<VAR>x : HahnSeries Γ R<VAR>s : HahnSeries.SummableFamily Γ R α<GOAL>(x • s).hsum = x * s.hsum
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>OrderedCancelAddCommMonoid Γ<VAR>Semiring R<VAR>α : Type u_3<VAR>s : HahnSeries.SummableFamily Γ R α<GOAL>HahnSeries.SummableFamily.lsum s = s.hsum
<VAR>Γ : Type u_1<VAR>OrderedCancelAddCommMonoid Γ<VAR>α : Type u_3<VAR>R : Type u_4<VAR>Ring R<VAR>s t : HahnSeries.SummableFamily Γ R α<GOAL>(s - t).hsum = s.hsum - t.hsum
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<GOAL>⇑(HahnSeries.SummableFamily.ofFinsupp f) = ⇑f
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>f : α →₀ HahnSeries Γ R<GOAL>(HahnSeries.SummableFamily.ofFinsupp f).hsum = f.sum fun x => id
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : HahnSeries.SummableFamily Γ R α<VAR>f : α ↪ β<VAR>b : β<GOAL>(s.embDomain f) b = if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : HahnSeries.SummableFamily Γ R α<VAR>f : α ↪ β<VAR>a : α<GOAL>(s.embDomain f) (f a) = s a
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : HahnSeries.SummableFamily Γ R α<VAR>f : α ↪ β<VAR>b : β<VAR>h : b ∉ Set.range ⇑f<GOAL>(s.embDomain f) b = 0
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>PartialOrder Γ<VAR>AddCommMonoid R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>s : HahnSeries.SummableFamily Γ R α<VAR>f : α ↪ β<GOAL>(s.embDomain f).hsum = s.hsum
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>CommRing R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>⇑(HahnSeries.SummableFamily.powers x hx) = HPow.hPow x
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>CommRing R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>(x • HahnSeries.SummableFamily.powers x hx).embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } = HahnSeries.SummableFamily.powers x hx - HahnSeries.SummableFamily.ofFinsupp (Finsupp.single 0 1)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>CommRing R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : 0 < x.orderTop<GOAL>(1 - x) * (HahnSeries.SummableFamily.powers x hx).hsum = 1
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedAddCommGroup Γ<VAR>CommRing R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<VAR>r : R<VAR>hr : r * x.leadingCoeff = 1<GOAL>0 < (1 - (HahnSeries.single (-x.order)) r * x).orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedAddCommGroup Γ<VAR>CommRing R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<GOAL>IsUnit x ↔ IsUnit x.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<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>Module.Flat R S<VAR>I : Ideal R<GOAL>↑R (Module.Flat.auxLTensor R S M I) = ↑(TensorProduct.rid R M) ∘ₗ LinearMap.lTensor M (Submodule.subtype I)
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<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>Module.Flat R S<VAR>Module.Flat S M<GOAL>Module.Flat R M
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal S<GOAL>Module.Flat.auxRTensorBaseChange R S M I = LinearMap.rTensor (S ⊗[R] M) (Submodule.subtype I)
<VAR>R : Type u<VAR>S : Type v<VAR>M : Type w<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Flat R M<VAR>N : Type t<VAR>AddCommGroup N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>f : M →ₗ[R] N<VAR>h : IsBaseChange S f<GOAL>Module.Flat S N
<VAR>R : Type u<VAR>M : Type u_1<VAR>Mp : Type u_2<VAR>Rp : Type v<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommRing Rp<VAR>Algebra R Rp<VAR>AddCommGroup Mp<VAR>Module R Mp<VAR>Module Rp Mp<VAR>IsScalarTower R Rp Mp<VAR>Module.Flat R M<VAR>S : Submonoid R<VAR>IsLocalization S Rp<VAR>f : M →ₗ[R] Mp<VAR>h : IsLocalizedModule S f<GOAL>Module.Flat Rp Mp
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>I : Ideal (MvPolynomial σ k)<VAR>x : σ → k<GOAL>x ∈ MvPolynomial.zeroLocus I ↔ ∀ p ∈ I, (MvPolynomial.eval x) p = 0
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>I J : Ideal (MvPolynomial σ k)<VAR>h : I ≤ J<GOAL>MvPolynomial.zeroLocus J ≤ MvPolynomial.zeroLocus I
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<GOAL>MvPolynomial.zeroLocus ⊥ = ⊤
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<GOAL>MvPolynomial.zeroLocus ⊤ = ⊥
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>V : Set (σ → k)<VAR>p : MvPolynomial σ k<GOAL>p ∈ MvPolynomial.vanishingIdeal V ↔ ∀ x ∈ V, (MvPolynomial.eval x) p = 0
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>A B : Set (σ → k)<VAR>h : A ≤ B<GOAL>MvPolynomial.vanishingIdeal B ≤ MvPolynomial.vanishingIdeal A
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<GOAL>MvPolynomial.vanishingIdeal ∅ = ⊤
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>I : Ideal (MvPolynomial σ k)<GOAL>I ≤ MvPolynomial.vanishingIdeal (MvPolynomial.zeroLocus I)
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>V : Set (σ → k)<GOAL>V ≤ MvPolynomial.zeroLocus (MvPolynomial.vanishingIdeal V)
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<GOAL>GaloisConnection MvPolynomial.zeroLocus MvPolynomial.vanishingIdeal
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>V : Set (σ → k)<VAR>I : Ideal (MvPolynomial σ k)<GOAL>V ≤ MvPolynomial.zeroLocus I ↔ I ≤ MvPolynomial.vanishingIdeal V