ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>S : Set (MvPolynomial σ k)<GOAL>MvPolynomial.zeroLocus (Ideal.span S) = {x | ∀ p ∈ S, (MvPolynomial.eval x) p = 0}
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>x : σ → k<VAR>p : MvPolynomial σ k<GOAL>p ∈ MvPolynomial.vanishingIdeal {x} ↔ (MvPolynomial.eval x) p = 0
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>I : Ideal (MvPolynomial σ k)<GOAL>I.radical ≤ MvPolynomial.vanishingIdeal (MvPolynomial.zeroLocus I)
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>V : Set (σ → k)<GOAL>PrimeSpectrum.vanishingIdeal (MvPolynomial.pointToPoint '' V) = MvPolynomial.vanishingIdeal V
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>I : Ideal (MvPolynomial σ k)<GOAL>MvPolynomial.pointToPoint '' MvPolynomial.zeroLocus I ≤ PrimeSpectrum.zeroLocus ↑I
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>IsAlgClosed k<VAR>Finite σ<VAR>I : Ideal (MvPolynomial σ k)<GOAL>I.IsMaximal ↔ ∃ x, I = MvPolynomial.vanishingIdeal {x}
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>IsAlgClosed k<VAR>Finite σ<VAR>I : Ideal (MvPolynomial σ k)<GOAL>MvPolynomial.vanishingIdeal (MvPolynomial.zeroLocus I) = I.radical
<VAR>k : Type u_1<VAR>Field k<VAR>σ : Type u_2<VAR>IsAlgClosed k<VAR>Finite σ<VAR>P : Ideal (MvPolynomial σ k)<VAR>h : P.IsPrime<GOAL>MvPolynomial.vanishingIdeal (MvPolynomial.zeroLocus P) = P
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<GOAL>I ≤ I.jacobson
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<GOAL>I.jacobson.jacobson = I.jacobson
<VAR>R : Type u<VAR>Ring R<GOAL>⊤.jacobson = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<GOAL>I.jacobson = ⊤ ↔ I = ⊤
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<GOAL>I.jacobson = ⊥ → I = ⊥
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<VAR>H : I.IsMaximal<GOAL>I.jacobson = I
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<VAR>x : R<GOAL>x ∈ I.jacobson ↔ ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<VAR>r : R<VAR>h : r - 1 ∈ I.jacobson<GOAL>∃ s, s * r - 1 ∈ I
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<GOAL>I.jacobson = I ↔ ∃ M, (∀ J ∈ M, J.IsMaximal ∨ J = ⊤) ∧ I = sInf M
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<GOAL>I.jacobson = I ↔ ∃ M, (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<GOAL>I.jacobson = I ↔ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>RingHom.ker f ≤ I → Ideal.map f I.jacobson = (Ideal.map f I).jacobson
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>hf : Function.Bijective ⇑f<GOAL>Ideal.map f I.jacobson = (Ideal.map f I).jacobson
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>K : Ideal S<GOAL>Ideal.comap f K.jacobson = sInf (Ideal.comap f '' {J | K ≤ J ∧ J.IsMaximal})
<VAR>R : Type u<VAR>S : Type v<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>K : Ideal S<GOAL>Ideal.comap f K.jacobson = (Ideal.comap f K).jacobson
<VAR>R : Type u<VAR>Ring R<VAR>I J : Ideal R<GOAL>I ≤ J → I.jacobson ≤ J.jacobson
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.radical ≤ I.jacobson
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>h : I.jacobson = I<GOAL>I.IsRadical
<VAR>R : Type u<VAR>CommRing R<VAR>r : R<VAR>h : r - 1 ∈ ⊥.jacobson<GOAL>IsUnit r
<VAR>R : Type u<VAR>CommRing R<VAR>x : R<GOAL>x ∈ ⊥.jacobson ↔ ∀ (y : R), IsUnit (x * y + 1)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.jacobson = I ↔ ⊥.jacobson = ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.radical = I.jacobson ↔ ⊥.radical = ⊥.jacobson
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.radical.jacobson = I.jacobson
<VAR>R : Type u<VAR>CommRing R<GOAL>⊥.jacobson ≤ sInf (Ideal.map Polynomial.C '' {J | J.IsMaximal})
<VAR>R : Type u<VAR>CommRing R<VAR>h : ⊥.jacobson = ⊥<GOAL>⊥.jacobson = ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>self : I.IsLocal<GOAL>I.jacobson.IsMaximal
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.IsLocal ↔ I.jacobson.IsMaximal
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>hi : I.radical.IsMaximal<GOAL>I.IsLocal
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>hi : I.IsLocal<VAR>hij : I ≤ J<VAR>hj : J ≠ ⊤<GOAL>J ≤ I.jacobson
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>hi : I.IsLocal<VAR>x : R<GOAL>x ∈ I.jacobson ∨ ∃ y, y * x - 1 ∈ I
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>hi : I.radical.IsMaximal<GOAL>I.IsPrimary
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>r : R<VAR>s : S<GOAL>(r, s) ∈ I.prod J ↔ r ∈ I ∧ s ∈ J
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<GOAL>⊤.prod ⊤ = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal (R × S)<GOAL>I = (Ideal.map (RingHom.fst R S) I).prod (Ideal.map (RingHom.snd R S) I)
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>J : Ideal S<GOAL>Ideal.map (RingHom.fst R S) (I.prod J) = I
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>J : Ideal S<GOAL>Ideal.map (RingHom.snd R S) (I.prod J) = J
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>J : Ideal S<GOAL>Ideal.map (↑RingEquiv.prodComm) (I.prod J) = J.prod I
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>J : Ideal S<GOAL>Ideal.idealProdEquiv.symm (I, J) = I.prod J
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I I' : Ideal R<VAR>J J' : Ideal S<GOAL>I.prod J = I'.prod J' ↔ I = I' ∧ J = J'
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>h : (I.prod ⊤).IsPrime<GOAL>I.IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal S<VAR>h : (⊤.prod I).IsPrime<GOAL>I.IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>h : I.IsPrime<GOAL>(I.prod ⊤).IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal S<VAR>h : I.IsPrime<GOAL>(⊤.prod I).IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal R<VAR>J : Ideal S<GOAL>(I.prod J).IsPrime → I = ⊤ ∨ J = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>I : Ideal (R × S)<GOAL>I.IsPrime ↔ (∃ p, p.IsPrime ∧ I = p.prod ⊤) ∨ ∃ p, p.IsPrime ∧ I = ⊤.prod p
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>h : I.FG<GOAL>IsIdempotentElem I ↔ ∃ e, IsIdempotentElem e ∧ I = Submodule.span R {e}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>I : Ideal R<VAR>h : I.FG<GOAL>IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommSemiring R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>b : Basis ι R S<VAR>x : S<VAR>hx : x ≠ 0<VAR>i : ι<GOAL>↑((Ideal.basisSpanSingleton b hx) i) = x * b i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommSemiring R<VAR>CommRing S<VAR>IsDomain S<VAR>Algebra R S<VAR>N : Type u_4<VAR>Semiring N<VAR>Module N S<VAR>SMulCommClass R N S<VAR>b : Basis ι R S<VAR>x : S<VAR>hx : x ≠ 0<GOAL>(↑(b.constr N)).toFun (Subtype.val ∘ ⇑(Ideal.basisSpanSingleton b hx)) = (Algebra.lmul R S) x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>I : Ideal S<VAR>b : Basis ι R ↥I<VAR>x : S<GOAL>x ∈ I ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Fintype ι<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>I : Ideal S<VAR>b : Basis ι R ↥I<VAR>x : S<GOAL>x ∈ I ↔ ∃ c, x = ∑ i : ι, c i • ↑(b i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>I ∈ Ideal.isPrincipalSubmonoid R ↔ Submodule.IsPrincipal I
<VAR>R : Type u_1<VAR>CommRing R<VAR>a : R<GOAL>Ideal.span {a} ∈ Ideal.isPrincipalSubmonoid R
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>x : R<GOAL>↑((Ideal.associatesEquivIsPrincipal R) (Associates.mk x)) = Ideal.span {x}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>I : Ideal R<VAR>hI : Submodule.IsPrincipal I<GOAL>(Ideal.associatesEquivIsPrincipal R).symm ⟨I, hI⟩ = Associates.mk (Submodule.IsPrincipal.generator I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>x y : Associates R<GOAL>↑((Ideal.associatesEquivIsPrincipal R) (x * y)) = ↑((Ideal.associatesEquivIsPrincipal R) x) * ↑((Ideal.associatesEquivIsPrincipal R) y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>↑((Ideal.associatesEquivIsPrincipal R) 0) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>↑((Ideal.associatesEquivIsPrincipal R) 1) = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>x : ↥(nonZeroDivisors R)<GOAL>↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) (Associates.mk x)) = Ideal.span {↑x}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>x : Associates ↥(nonZeroDivisors R)<GOAL>↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) x) = ↑((Ideal.associatesEquivIsPrincipal R) ↑(associatesNonZeroDivisorsEquiv.symm x))
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>x y : Associates ↥(nonZeroDivisors R)<GOAL>↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) (x * y)) = ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) x) * ↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>↑↑((Ideal.associatesNonZeroDivisorsEquivIsPrincipal R) 1) = 1
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f g : Ring.Perfection R p<VAR>h : ∀ (n : ℕ), (Perfection.coeff R p n) f = (Perfection.coeff R p n) g<GOAL>f = g
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : ℕ → R<VAR>hf : ∀ (n : ℕ), f (n + 1) ^ p = f n<VAR>n : ℕ<GOAL>(Perfection.coeff R p n) ⟨f, hf⟩ = f n
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(Perfection.coeff R p n) ((Perfection.pthRoot R p) f) = (Perfection.coeff R p (n + 1)) f
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(Perfection.coeff R p (n + 1)) (f ^ p) = (Perfection.coeff R p n) f
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(Perfection.coeff R p (n + 1)) f ^ p = (Perfection.coeff R p n) f
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(Perfection.coeff R p (n + 1)) ((frobenius (Ring.Perfection R p) p) f) = (Perfection.coeff R p n) f
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : Ring.Perfection R p<VAR>n m : ℕ<GOAL>(Perfection.coeff R p (n + m)) ((⇑(frobenius (Ring.Perfection R p) p))^[m] f) = (Perfection.coeff R p n) f
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : Ring.Perfection R p<VAR>n m : ℕ<VAR>hmn : m ≤ n<GOAL>(Perfection.coeff R p n) ((⇑(frobenius (Ring.Perfection R p) p))^[m] f) = (Perfection.coeff R p (n - m)) f
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<GOAL>(Perfection.pthRoot R p).comp (frobenius (Ring.Perfection R p) p) = RingHom.id (Ring.Perfection R p)
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<GOAL>(frobenius (Ring.Perfection R p) p).comp (Perfection.pthRoot R p) = RingHom.id (Ring.Perfection R p)
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : Ring.Perfection R p<VAR>n : ℕ<VAR>hfn : (Perfection.coeff R p n) f ≠ 0<VAR>k : ℕ<GOAL>(Perfection.coeff R p (n + k)) f ≠ 0
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>f : Ring.Perfection R p<VAR>m n : ℕ<VAR>hfm : (Perfection.coeff R p m) f ≠ 0<VAR>hmn : m ≤ n<GOAL>(Perfection.coeff R p n) f ≠ 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>PerfectRing R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>f : R →+* Ring.Perfection S p<GOAL>(Perfection.lift p R S).symm f = (Perfection.coeff S p 0).comp f
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>PerfectRing R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>f : R →+* S<VAR>r : R<VAR>n : ℕ<GOAL>↑(((Perfection.lift p R S) f) r) n = f ((⇑↑(frobeniusEquiv R p).symm)^[n] r)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>PerfectRing R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>f g : R →+* Ring.Perfection S p<VAR>hfg : ∀ (x : R), (Perfection.coeff S p 0) (f x) = (Perfection.coeff S p 0) (g x)<GOAL>f = g
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>φ : R →+* S<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>↑((Perfection.map p φ) f) n = φ ((Perfection.coeff R p n) f)
<VAR>R : Type u₁<VAR>CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>φ : R →+* S<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(Perfection.coeff S p n) ((Perfection.map p φ) f) = φ ((Perfection.coeff R p n) f)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₂<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* R<VAR>self : PerfectionMap p π<VAR>f : ℕ → R<GOAL>(∀ (n : ℕ), f (n + 1) ^ p = f n) → ∃ x, ∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = f n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₂<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* R<VAR>self : PerfectionMap p π<VAR>x y : P<GOAL>(∀ (n : ℕ), π ((⇑(frobeniusEquiv P p).symm)^[n] x) = π ((⇑(frobeniusEquiv P p).symm)^[n] y)) → x = y
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>f : P →+* R<VAR>g : P ≃+* Ring.Perfection R p<VAR>hfg : (Perfection.lift p P R) f = ↑g<GOAL>PerfectionMap p f
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<GOAL>PerfectionMap p (Perfection.coeff R p 0)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>PerfectRing R p<GOAL>PerfectionMap p (RingHom.id R)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* R<VAR>m : PerfectionMap p π<VAR>x : P<GOAL>m.equiv x = ((Perfection.lift p P R) π) x
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* R<VAR>m : PerfectionMap p π<VAR>x : P<GOAL>(Perfection.coeff R p 0) (m.equiv x) = π x
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* R<VAR>m : PerfectionMap p π<GOAL>(Perfection.coeff R p 0).comp ↑m.equiv = π
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* R<VAR>m : PerfectionMap p π<VAR>f : Ring.Perfection R p<GOAL>π (m.equiv.symm f) = (Perfection.coeff R p 0) f
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* R<VAR>m : PerfectionMap p π<GOAL>π.comp ↑m.equiv.symm = Perfection.coeff R p 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>PerfectRing R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* S<VAR>m : PerfectionMap p π<VAR>f : R →+* S<GOAL>(PerfectionMap.lift p R S P π m) f = (↑m.equiv.symm).comp ((Perfection.lift p R S) f)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>PerfectRing R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* S<VAR>m : PerfectionMap p π<VAR>f : R →+* P<GOAL>(PerfectionMap.lift p R S P π m).symm f = π.comp f
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>PerfectRing R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>π : P →+* S<VAR>m : PerfectionMap p π<VAR>f g : R →+* P<VAR>hfg : ∀ (x : R), π (f x) = π (g x)<GOAL>f = g
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>Q : Type u₄<VAR>CommSemiring Q<VAR>CharP Q p<VAR>PerfectRing Q p<VAR>π : P →+* R<VAR>m : PerfectionMap p π<VAR>σ : Q →+* S<VAR>n : PerfectionMap p σ<VAR>φ : R →+* S<GOAL>σ.comp (PerfectionMap.map p m n φ) = φ.comp π
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>P : Type u₃<VAR>CommSemiring P<VAR>CharP P p<VAR>PerfectRing P p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>Q : Type u₄<VAR>CommSemiring Q<VAR>CharP Q p<VAR>PerfectRing Q p<VAR>π : P →+* R<VAR>m : PerfectionMap p π<VAR>σ : Q →+* S<VAR>n : PerfectionMap p σ<VAR>φ : R →+* S<VAR>x : P<GOAL>σ ((PerfectionMap.map p m n φ) x) = φ (π x)
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>R : Type u₁<VAR>CommSemiring R<VAR>CharP R p<VAR>S : Type u₂<VAR>CommSemiring S<VAR>CharP S p<VAR>φ : R →+* S<GOAL>PerfectionMap.map p ⋯ ⋯ φ = Perfection.map p φ
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>x : O<VAR>hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0<GOAL>ModP.preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<GOAL>ModP.preVal K v O hv p 0 = 0
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>x y : ModP K v O hv p<VAR>hxy0 : x * y ≠ 0<GOAL>ModP.preVal K v O hv p (x * y) = ModP.preVal K v O hv p x * ModP.preVal K v O hv p y
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>x y : ModP K v O hv p<GOAL>ModP.preVal K v O hv p (x + y) ≤ max (ModP.preVal K v O hv p x) (ModP.preVal K v O hv p y)
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>x : ModP K v O hv p<GOAL>v ↑p < ModP.preVal K v O hv p x ↔ x ≠ 0
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>x : ModP K v O hv p<GOAL>ModP.preVal K v O hv p x = 0 ↔ x = 0
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>x : O<GOAL>v ↑p < v ((algebraMap O K) x) ↔ (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x y : ModP K v O hv p<VAR>hx : x ^ p ≠ 0<VAR>hy : y ^ p ≠ 0<GOAL>x * y ≠ 0
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<VAR>h : ∃ n, (Perfection.coeff (ModP K v O hv p) p n) f ≠ 0<VAR>k : ℕ<GOAL>(Perfection.coeff (ModP K v O hv p) p (Nat.find h + k)) f ≠ 0
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<VAR>n : ℕ<VAR>hfn : (Perfection.coeff (ModP K v O hv p) p n) f ≠ 0<GOAL>PreTilt.valAux K v O hv p f = ModP.preVal K v O hv p ((Perfection.coeff (ModP K v O hv p) p n) f) ^ p ^ n
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<GOAL>PreTilt.valAux K v O hv p 0 = 0
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<GOAL>PreTilt.valAux K v O hv p 1 = 1
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<GOAL>PreTilt.valAux K v O hv p (f * g) = PreTilt.valAux K v O hv p f * PreTilt.valAux K v O hv p g
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f g : PreTilt K v O hv p<GOAL>PreTilt.valAux K v O hv p (f + g) ≤ max (PreTilt.valAux K v O hv p f) (PreTilt.valAux K v O hv p g)
<VAR>K : Type u₁<VAR>Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>CommRing O<VAR>Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>f : PreTilt K v O hv p<GOAL>(PreTilt.val K v O hv p) f = 0 ↔ f = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N P : Submodule R M<VAR>r : R<GOAL>r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N P : Submodule R M<VAR>r : R<GOAL>r ∈ N.colon P ↔ P ≤ Submodule.comap (r • LinearMap.id) N
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>Submodule.colon I ⊤ = I
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<GOAL>⊥.colon N = N.annihilator
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N₁ N₂ P₁ P₂ : Submodule R M<VAR>hn : N₁ ≤ N₂<VAR>hp : P₁ ≤ P₂<GOAL>N₁.colon P₂ ≤ N₂.colon P₁
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι₁ : Sort u_6<VAR>f : ι₁ → Submodule R M<VAR>ι₂ : Sort u_7<VAR>g : ι₂ → Submodule R M<GOAL>(⨅ i, f i).colon (⨆ j, g j) = ⨅ i, ⨅ j, (f i).colon (g j)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>x : M<VAR>r : R<GOAL>r ∈ N.colon (Submodule.span R {x}) ↔ r • x ∈ N
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>x r : R<GOAL>r ∈ Submodule.colon I (Ideal.span {x}) ↔ r * x ∈ I
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<GOAL>Module.annihilator R (M ⧸ N) = N.colon ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<GOAL>Module.annihilator R (R ⧸ I) = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<GOAL>I ∈ associatedPrimes R M ↔ IsAssociatedPrime I M
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>h : IsAssociatedPrime I M<GOAL>I.IsPrime
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>h : IsAssociatedPrime I M<VAR>hf : Function.Injective ⇑f<GOAL>IsAssociatedPrime I M'
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>l : M ≃ₗ[R] M'<GOAL>IsAssociatedPrime I M ↔ IsAssociatedPrime I M'
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Subsingleton M<GOAL>¬IsAssociatedPrime I M
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>H : IsNoetherianRing R<VAR>x : M<VAR>hx : x ≠ 0<GOAL>∃ P, IsAssociatedPrime P M ∧ (Submodule.span R {x}).annihilator ≤ P