ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>CommRing S<VAR>L : Type u_3<VAR>Field L<VAR>Algebra R S<VAR>Algebra S L<VAR>Algebra R L<VAR>IsScalarTower R S L<VAR>IsIntegralClosure S R L<VAR>Algebra.IsAlgebraic R L<VAR>inj : Function.Injective ⇑(algebraMap R L)<VAR>a : S<VAR>b : S<VAR>hb : b ≠ 0<GOAL>∃ c d, d ≠ 0 ∧ d • a = b * c
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>p : K[X]<VAR>aeval_ne : (Polynomial.aeval x) p.divX ≠ 0<GOAL>x⁻¹ = (Polynomial.aeval x) p.divX / ((Polynomial.aeval x) p - (algebraMap K L) (p.coeff 0))
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>p : K[X]<VAR>aeval_eq : (Polynomial.aeval x) p = 0<VAR>coeff_zero_ne : p.coeff 0 ≠ 0<GOAL>x⁻¹ = -((Polynomial.aeval x) p.divX / (algebraMap K L) (p.coeff 0))
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>A : Subalgebra K L<VAR>x : ↥A<VAR>p : K[X]<VAR>aeval_eq : (Polynomial.aeval x) p = 0<VAR>coeff_zero_ne : p.coeff 0 ≠ 0<GOAL>(↑x)⁻¹ ∈ A
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>A : Subalgebra K L<VAR>x : ↥A<VAR>hx : IsAlgebraic K ↑x<GOAL>(↑x)⁻¹ ∈ A
<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>A : Subalgebra K L<VAR>Algebra.IsAlgebraic K L<GOAL>IsField ↥A
<VAR>R' : Type u<VAR>S' : Type v<VAR>Semiring R'<VAR>SMul R' S'<VAR>p : R'[X]<VAR>f : R' → S'<VAR>x : R'<GOAL>(p • f) x = Polynomial.eval x p • f x
<VAR>R' : Type u<VAR>S' : Type v<VAR>T' : Type w<VAR>CommSemiring R'<VAR>Semiring S'<VAR>Algebra R' S'<VAR>SMul S' T'<VAR>p : R'[X]<VAR>f : S' → T'<VAR>x : S'<GOAL>(p • f) x = (Polynomial.aeval x) p • f x
<VAR>R' : Type u<VAR>S' : Type v<VAR>T' : Type w<VAR>CommSemiring R'<VAR>CommSemiring S'<VAR>CommSemiring T'<VAR>Algebra R' S'<VAR>Algebra S' T'<GOAL>⇑(algebraMap R'[X] (S' → T')) = fun p z => (algebraMap S' T') ((Polynomial.aeval z) p)
<VAR>R' : Type u<VAR>CommSemiring R'<GOAL>⇑(algebraMap R'[X] (R' → R')) = fun p z => Polynomial.eval z p
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : FractionalIdeal (nonZeroDivisors R) K<VAR>a : ↥(nonZeroDivisors R)<VAR>I₀ : Ideal R<VAR>h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀<GOAL>↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : FractionalIdeal (nonZeroDivisors R) K<GOAL>FractionalIdeal.absNorm I = ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den|
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : FractionalIdeal (nonZeroDivisors R) K<VAR>a : ↥(nonZeroDivisors R)<VAR>I₀ : Ideal R<VAR>h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀<GOAL>FractionalIdeal.absNorm I = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : FractionalIdeal (nonZeroDivisors R) K<GOAL>0 ≤ FractionalIdeal.absNorm I
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>FractionalIdeal.absNorm ⊥ = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>FractionalIdeal.absNorm 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>NoZeroDivisors K<VAR>I : FractionalIdeal (nonZeroDivisors R) K<GOAL>FractionalIdeal.absNorm I = 0 ↔ I = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I₀ : Ideal R<GOAL>FractionalIdeal.absNorm ↑I₀ = ↑(Ideal.absNorm I₀)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsLocalization (Algebra.algebraMapSubmonoid R (nonZeroDivisors ℤ)) K<VAR>Algebra ℚ K<VAR>NoZeroDivisors K<VAR>ι : Type u_3<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι ℤ R<VAR>I : FractionalIdeal (nonZeroDivisors R) K<VAR>bI : Basis ι ℤ ↥↑I<GOAL>|(Basis.localizationLocalization ℚ (nonZeroDivisors ℤ) K b).det (Subtype.val ∘ ⇑bI)| = FractionalIdeal.absNorm I
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Module.Free ℤ R<VAR>Module.Finite ℤ R<VAR>K : Type u_2<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsLocalization (Algebra.algebraMapSubmonoid R (nonZeroDivisors ℤ)) K<VAR>Algebra ℚ K<VAR>Module.Finite ℚ K<VAR>x : K<GOAL>FractionalIdeal.absNorm (FractionalIdeal.spanSingleton (nonZeroDivisors R) x) = |(Algebra.norm ℚ) x|
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>R : Type u_1<VAR>CommRing R<VAR>CharP R p<VAR>i : ℕ<VAR>hin : i ≤ n<VAR>hpi : ↑p ^ i = 0<GOAL>i = n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>CharP (TruncatedWittVector p n (ZMod p)) (p ^ n)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>x : ZMod (p ^ n)<GOAL>(TruncatedWittVector.zmodEquivTrunc p n) x = (ZMod.castHom ⋯ (TruncatedWittVector p n (ZMod p))) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>(TruncatedWittVector.truncate hm).comp (TruncatedWittVector.zmodEquivTrunc p m).toRingHom = (TruncatedWittVector.zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : ZMod (p ^ m)<GOAL>(TruncatedWittVector.truncate hm) ((TruncatedWittVector.zmodEquivTrunc p m) x) = (TruncatedWittVector.zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>m : ℕ<VAR>hm : n ≤ m<VAR>x : TruncatedWittVector p m (ZMod p)<GOAL>(TruncatedWittVector.zmodEquivTrunc p n).symm ((TruncatedWittVector.truncate hm) x) = (ZMod.castHom ⋯ (ZMod (p ^ n))) ((TruncatedWittVector.zmodEquivTrunc p m).symm x)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>m : ℕ<VAR>hm : n ≤ m<GOAL>(TruncatedWittVector.zmodEquivTrunc p n).symm.toRingHom.comp (TruncatedWittVector.truncate hm) = (ZMod.castHom ⋯ (ZMod (p ^ n))).comp (TruncatedWittVector.zmodEquivTrunc p m).symm.toRingHom
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m n : ℕ<VAR>h : m ≤ n<GOAL>(ZMod.castHom ⋯ (ZMod (p ^ m))).comp (WittVector.toZModPow p n) = WittVector.toZModPow p m
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k₁ k₂ : ℕ<VAR>hk : k₁ ≤ k₂<GOAL>(TruncatedWittVector.truncate hk).comp ((TruncatedWittVector.zmodEquivTrunc p k₂).toRingHom.comp (PadicInt.toZModPow k₂)) = (TruncatedWittVector.zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(WittVector.toPadicInt p).comp (WittVector.fromPadicInt p) = RingHom.id ℤ_[p]
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : ℤ_[p]<GOAL>((WittVector.toPadicInt p).comp (WittVector.fromPadicInt p)) x = (RingHom.id ℤ_[p]) x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>(WittVector.fromPadicInt p).comp (WittVector.toPadicInt p) = RingHom.id (𝕎 (ZMod p))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : 𝕎 (ZMod p)<GOAL>((WittVector.fromPadicInt p).comp (WittVector.toPadicInt p)) x = (RingHom.id (𝕎 (ZMod p))) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>IsFractional S ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>I.den • ↑I = Submodule.map (Algebra.linearMap R P) I.num
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<VAR>x : P<GOAL>x ∈ ↑I ↔ x ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>(∀ (x : P), x ∈ I ↔ x ∈ J) → I = J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>Nontrivial P<VAR>NoZeroSMulDivisors R P<VAR>I : FractionalIdeal S P<VAR>h_nz : ↑I.den ≠ 0<VAR>x : ↥I<GOAL>(algebraMap R P) ↑((FractionalIdeal.equivNum h_nz) x) = I.den • ↑x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>p : FractionalIdeal S P<VAR>s : Set P<VAR>hs : s = ↑p<GOAL>↑(p.copy s hs) = s
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>p : FractionalIdeal S P<VAR>s : Set P<VAR>hs : s = ↑p<GOAL>p.copy s hs = p
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>0 ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>↑I = ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Submodule R P<VAR>hI : IsFractional S I<GOAL>↑⟨I, hI⟩ = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>↑↑I = ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>Function.Injective fun I => ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>↑I = ↑J ↔ I = J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Submodule R P<VAR>h : I ≤ 1<GOAL>IsFractional S I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Submodule R P<VAR>J : FractionalIdeal S P<VAR>hIJ : I ≤ ↑J<GOAL>IsFractional S I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Ideal R<GOAL>↑↑I = IsLocalization.coeSubmodule P I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>x : P<VAR>I : Ideal R<GOAL>x ∈ ↑I ↔ ∃ x' ∈ I, (algebraMap R P) x' = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>x : R<VAR>I : Ideal R<VAR>hx : x ∈ I<GOAL>(algebraMap R P) x ∈ ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>IsLocalization S P<VAR>h : S ≤ R⁰<VAR>I J : Ideal R<GOAL>↑I ≤ ↑J ↔ I ≤ J
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I J : Ideal R<GOAL>↑I ≤ ↑J ↔ I ≤ J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>x : P<GOAL>x ∈ 0 ↔ x = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>↑0 = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>↑⊥ = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>x : R<VAR>I : Ideal R<VAR>h : S ≤ R⁰<GOAL>(∃ x' ∈ I, (algebraMap R P) x' = (algebraMap R P) x) ↔ x ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>h : S ≤ R⁰<GOAL>Function.Injective fun I => ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>h : S ≤ R⁰<VAR>I J : Ideal R<GOAL>↑I = ↑J ↔ I = J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Ideal R<VAR>h : S ≤ R⁰<GOAL>↑I = 0 ↔ I = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>loc : IsLocalization S P<VAR>I : Ideal R<VAR>h : S ≤ R⁰<GOAL>↑I ≠ 0 ↔ I ≠ ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>↑I = ⊥ ↔ I = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>↑I ≠ ⊥ ↔ I ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>NoZeroSMulDivisors R P<VAR>hS : 0 ∉ S<VAR>I : FractionalIdeal S P<VAR>hI : I.num = ⊥<GOAL>I = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>h_inj : Function.Injective ⇑(algebraMap R P)<GOAL>FractionalIdeal.num 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>↑⊤ = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>x : P<GOAL>x ∈ 1 ↔ ∃ x', (algebraMap R P) x' = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>x : R<GOAL>(algebraMap R P) x ∈ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>1 ∈ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>↑1 = IsLocalization.coeSubmodule P ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>↑1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>↑I ≤ ↑J ↔ I ≤ J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>0 ≤ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<GOAL>⊥ = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>I ≤ 0 ↔ I = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>I = 0 ↔ ∀ x ∈ I, x = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : Submodule R P<GOAL>IsFractional S I → IsFractional S J → IsFractional S (I ⊔ J)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Submodule R P<GOAL>IsFractional S I → ∀ (J : Submodule R P), IsFractional S (I ⊓ J)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>↑(I ⊓ J) = ↑I ⊓ ↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>↑(I ⊔ J) = ↑I ⊔ ↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>I ⊔ J = I + J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>↑(I + J) = ↑I + ↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : Ideal R<GOAL>↑(I ⊔ J) = ↑I + ↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Submodule R P<VAR>n : ℕ<GOAL>IsFractional S I → IsFractional S (n • I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>n : ℕ<VAR>I : FractionalIdeal S P<GOAL>↑(n • I) = n • ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : Submodule R P<GOAL>IsFractional S I → IsFractional S J → IsFractional S (I * J)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Submodule R P<VAR>h : IsFractional S I<VAR>n : ℕ<GOAL>IsFractional S (I ^ n)
<VAR>R : Type u_3<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_4<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>I.mul J = ⟨↑I * ↑J, ⋯⟩
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>I.mul J = I * J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>I * J = ⟨↑I * ↑J, ⋯⟩
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<GOAL>↑(I * J) = ↑I * ↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : Ideal R<GOAL>↑(I * J) = ↑I * ↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>Monotone fun x => I * x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>Monotone fun J => J * I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<VAR>i j : P<VAR>hi : i ∈ I<VAR>hj : j ∈ J<GOAL>i * j ∈ I * J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J K : FractionalIdeal S P<GOAL>I * J ≤ K ↔ ∀ i ∈ I, ∀ j ∈ J, i * j ∈ K
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<VAR>n : ℕ<GOAL>↑(I ^ n) = ↑I ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<VAR>C : P → Prop<VAR>r : P<VAR>hr : r ∈ I * J<VAR>hm : ∀ i ∈ I, ∀ j ∈ J, C (i * j)<VAR>ha : ∀ (x y : P), C x → C y → C (x + y)<GOAL>C r
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>(FractionalIdeal.coeSubmoduleHom S P) I = ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<VAR>hIJ : I ≤ J<VAR>J' : FractionalIdeal S P<GOAL>J' + I ≤ J' + J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I J : FractionalIdeal S P<VAR>hIJ : I ≤ J<VAR>J' : FractionalIdeal S P<GOAL>J' * I ≤ J' * J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<VAR>hI : 1 ≤ I<GOAL>I ≤ I * I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<VAR>hI : I ≤ 1<GOAL>I * I ≤ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Ideal R<GOAL>↑I ≤ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>J : FractionalIdeal S P<GOAL>J ≤ 1 ↔ ∃ I, ↑I = J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : FractionalIdeal S P<GOAL>1 ≤ I ↔ 1 ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Ideal R<GOAL>(FractionalIdeal.coeIdealHom S P) I = ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>I : Ideal R<VAR>n : ℕ<GOAL>↑(I ^ n) = ↑I ^ n
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>CommRing P<VAR>Algebra R P<VAR>IsLocalization S P<VAR>α : Sort u_3<VAR>f : α → Ideal R<VAR>hS : S ≤ R⁰<GOAL>↑(∏ᶠ (a : α), f a) = ∏ᶠ (a : α), ↑(f a)
<VAR>R : Type u_3<VAR>CommRing R<VAR>Nontrivial R<VAR>S : Submonoid R<VAR>P : Type u_4<VAR>Nontrivial P<VAR>CommRing P<VAR>Algebra R P<VAR>NoZeroSMulDivisors R P<VAR>hR : IsNoetherianRing R<VAR>hS : S ≤ R⁰<VAR>I : FractionalIdeal S P<GOAL>(↑I).FG
<VAR>p : ℕ<VAR>R : Type u_1<VAR>x y : 𝕎 R<VAR>h : ∀ (n : ℕ), x.coeff n = y.coeff n<GOAL>x = y
<VAR>p : ℕ<VAR>R : Type u_1<VAR>x y : 𝕎 R<GOAL>x = y ↔ ∀ (n : ℕ), x.coeff n = y.coeff n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>x : ℕ → R<GOAL>(WittVector.mk p x).coeff = x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>WittVector.wittZero p n = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>WittVector.wittOne p 0 = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>WittVector.wittOne p n = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>WittVector.wittAdd p 0 = MvPolynomial.X (0, 0) + MvPolynomial.X (1, 0)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>WittVector.wittSub p 0 = MvPolynomial.X (0, 0) - MvPolynomial.X (1, 0)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>WittVector.wittMul p 0 = MvPolynomial.X (0, 0) * MvPolynomial.X (1, 0)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>WittVector.wittNeg p 0 = -MvPolynomial.X (0, 0)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (WittVector.wittAdd p n) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (WittVector.wittSub p n) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (WittVector.wittMul p n) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (WittVector.wittNeg p n) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m n : ℕ<GOAL>MvPolynomial.constantCoeff (WittVector.wittNSMul p m n) = 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (WittVector.wittZSMul p z n) = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>n : ℕ<GOAL>WittVector.coeff 0 n = 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<GOAL>WittVector.coeff 1 0 = 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>WittVector.coeff 1 n = 0
<VAR>p' : ℕ<VAR>R' : Type u_2<VAR>x y : WittVector p' R'<VAR>i : Fin 2<GOAL>(![x, y] i).coeff = ![x.coeff, y.coeff] i
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>(x + y).coeff n = WittVector.peval (WittVector.wittAdd p n) ![x.coeff, y.coeff]
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>(x - y).coeff n = WittVector.peval (WittVector.wittSub p n) ![x.coeff, y.coeff]
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : 𝕎 R<VAR>n : ℕ<GOAL>(x * y).coeff n = WittVector.peval (WittVector.wittMul p n) ![x.coeff, y.coeff]
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(-x).coeff n = WittVector.peval (WittVector.wittNeg p n) ![x.coeff]
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(m • x).coeff n = WittVector.peval (WittVector.wittNSMul p m n) ![x.coeff]
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>m : ℤ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(m • x).coeff n = WittVector.peval (WittVector.wittZSMul p m n) ![x.coeff]
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>m : ℕ<VAR>x : 𝕎 R<VAR>n : ℕ<GOAL>(x ^ m).coeff n = WittVector.peval (WittVector.wittPow p m n) ![x.coeff]
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : 𝕎 R<GOAL>(x + y).coeff 0 = x.coeff 0 + y.coeff 0
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x y : 𝕎 R<GOAL>(x * y).coeff 0 = x.coeff 0 * y.coeff 0
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(WittVector.wittAdd p n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)