ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>k : ℕ<VAR>hk : a ^ k ∣ b<GOAL>↑k ≤ multiplicity a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>k : ℕ<GOAL>a ^ k ∣ b ↔ ↑k ≤ multiplicity a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>k : ℕ<GOAL>multiplicity a b < ↑k ↔ ¬a ^ k ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>n : ℕ<GOAL>multiplicity a b = ↑n ↔ a ^ n ∣ b ∧ ¬a ^ (n + 1) ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a b = ⊤ ↔ ∀ (n : ℕ), a ^ n ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>b : α<VAR>ha : IsUnit a<GOAL>multiplicity a b = ⊤
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>b : α<GOAL>multiplicity 1 b = ⊤
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : multiplicity.Finite a 1<GOAL>(multiplicity a 1).get ha = 0
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>u : αˣ<GOAL>multiplicity (↑u) a = ⊤
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a b = 0 ↔ ¬a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a b ≠ 0 ↔ a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a b = ⊤ ↔ ¬multiplicity.Finite a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a b ≠ ⊤ ↔ multiplicity.Finite a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a b < ⊤ ↔ multiplicity.Finite a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : multiplicity.Finite a b<GOAL>∃ c, b = a ^ (multiplicity a b).get hfin * c ∧ ¬a ∣ c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>Monoid β<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>c d : β<GOAL>multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>Monoid β<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>c d : β<GOAL>multiplicity a b = multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b ↔ c ^ n ∣ d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>Monoid β<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>F : Type u_3<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>a b : α<GOAL>multiplicity a b ≤ multiplicity (f a) (f b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Monoid α<VAR>Monoid β<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>F : Type u_3<VAR>EquivLike F α β<VAR>MulEquivClass F α β<VAR>f : F<VAR>a b : α<GOAL>multiplicity (f a) (f b) = multiplicity a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b c : α<VAR>h : b ∣ c<GOAL>multiplicity a b ≤ multiplicity a c
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b c : α<VAR>h : Associated b c<GOAL>multiplicity a b = multiplicity a c
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>h : 0 < multiplicity a b<GOAL>a ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>0 < multiplicity a b ↔ a ∣ b
<VAR>a b : ℕ<GOAL>multiplicity.Finite a b ↔ a ≠ 1 ∧ 0 < b
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>a b c : α<GOAL>multiplicity.Finite a (b * c) → multiplicity.Finite a c
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>ha : ¬IsUnit a<VAR>hb : IsUnit b<GOAL>multiplicity a b = 0
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : ¬IsUnit a<GOAL>multiplicity a 1 = 0
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : ¬IsUnit a<VAR>u : αˣ<GOAL>multiplicity a ↑u = 0
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b c : α<VAR>hdvd : a ∣ b<GOAL>multiplicity b c ≤ multiplicity a c
<VAR>α : Type u_1<VAR>CommMonoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b c : α<VAR>h : Associated a b<GOAL>multiplicity b c = multiplicity a c
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>a b : α<VAR>h : multiplicity.Finite a b<GOAL>b ≠ 0
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<GOAL>multiplicity a 0 = ⊤
<VAR>α : Type u_1<VAR>MonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : a ≠ 0<GOAL>multiplicity 0 a = 0
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity (Associates.mk a) (Associates.mk b) = multiplicity a b
<VAR>α : Type u_1<VAR>Semiring α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<GOAL>min (multiplicity p a) (multiplicity p b) ≤ multiplicity p (a + b)
<VAR>α : Type u_1<VAR>Ring α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity a (-b) = multiplicity a b
<VAR>a : ℕ<VAR>b : ℤ<GOAL>multiplicity a b.natAbs = multiplicity (↑a) b
<VAR>α : Type u_1<VAR>Ring α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p b < multiplicity p a<GOAL>multiplicity p (a + b) = multiplicity p b
<VAR>α : Type u_1<VAR>Ring α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p b < multiplicity p a<GOAL>multiplicity p (a - b) = multiplicity p b
<VAR>α : Type u_1<VAR>Ring α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>h : multiplicity p a ≠ multiplicity p b<GOAL>multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : α<VAR>hp : Prime p<VAR>a b : α<VAR>n m : ℕ<GOAL>¬p ^ (n + 1) ∣ a → ¬p ^ (m + 1) ∣ b → ¬p ^ (n + m + 1) ∣ a * b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p a b : α<VAR>hp : Prime p<GOAL>multiplicity.Finite p a → multiplicity.Finite p b → multiplicity.Finite p (a * b)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p a b : α<VAR>hp : Prime p<GOAL>multiplicity.Finite p (a * b) ↔ multiplicity.Finite p a ∧ multiplicity.Finite p b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p a : α<VAR>hp : Prime p<VAR>k : ℕ<GOAL>multiplicity.Finite p a → multiplicity.Finite p (a ^ k)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : ¬IsUnit a<VAR>ha0 : a ≠ 0<GOAL>multiplicity a a = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a : α<VAR>ha : multiplicity.Finite a a<GOAL>(multiplicity a a).get ha = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<VAR>h : (multiplicity p (a * b)).Dom<GOAL>(multiplicity p (a * b)).get h = (multiplicity p a).get ⋯ + (multiplicity p b).get ⋯
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p a b : α<VAR>hp : Prime p<GOAL>multiplicity p (a * b) = multiplicity p a + multiplicity p b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>β : Type u_3<VAR>p : α<VAR>hp : Prime p<VAR>s : Finset β<VAR>f : β → α<GOAL>multiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, multiplicity p (f x)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p a : α<VAR>hp : Prime p<VAR>ha : multiplicity.Finite p a<VAR>k : ℕ<GOAL>(multiplicity p (a ^ k)).get ⋯ = k * (multiplicity p a).get ha
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p a : α<VAR>hp : Prime p<VAR>k : ℕ<GOAL>multiplicity p (a ^ k) = k • multiplicity p a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p : α<VAR>h0 : p ≠ 0<VAR>hu : ¬IsUnit p<VAR>n : ℕ<GOAL>multiplicity p (p ^ n) = ↑n
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>p : α<VAR>hp : Prime p<VAR>n : ℕ<GOAL>multiplicity p (p ^ n) = ↑n
<VAR>p a b : ℕ<VAR>hp : p ≠ 1<VAR>hle : multiplicity p a ≤ multiplicity p b<VAR>hab : a.Coprime b<GOAL>multiplicity p a = 0
<VAR>a b : ℤ<GOAL>multiplicity.Finite a b ↔ multiplicity.Finite a.natAbs b.natAbs
<VAR>a b : ℤ<GOAL>multiplicity.Finite a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>{v | v.asIdeal ∣ I}.Finite
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>(Function.mulSupport fun v => v.maxPowDividing I).Finite
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>(Function.mulSupport fun v => ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors)).Finite
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>(Function.mulSupport fun v => ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk I).factors))).Finite
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣ ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I : Ideal R<GOAL>Associates.mk (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I) ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>(Associates.mk v.asIdeal).count (Associates.mk (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I)).factors = (Associates.mk v.asIdeal).count (Associates.mk I).factors
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)) = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>n : R<VAR>hn : n ≠ 0<VAR>d : ↥R⁰<GOAL>∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {n})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = FractionalIdeal.spanSingleton R⁰ (IsLocalization.mk' K n d)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>k : K<VAR>hk : I = FractionalIdeal.spanSingleton R⁰ k<GOAL>∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(Classical.choose ⋯)})).factors)) = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>FractionalIdeal.count K v 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<GOAL>FractionalIdeal.count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>h_aJ : I = FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>FractionalIdeal.count K v I = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>hI' : I' ≠ 0<GOAL>FractionalIdeal.count K v (I * I') = FractionalIdeal.count K v I + FractionalIdeal.count K v I'
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>I I' : FractionalIdeal R⁰ K<GOAL>FractionalIdeal.count K v (I * I') = if I ≠ 0 ∧ I' ≠ 0 then FractionalIdeal.count K v I + FractionalIdeal.count K v I' else 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>FractionalIdeal.count K v 1 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>I : ι → FractionalIdeal R⁰ K<VAR>hS : ∀ i ∈ s, I i ≠ 0<GOAL>FractionalIdeal.count K v (∏ i ∈ s, I i) = ∑ i ∈ s, FractionalIdeal.count K v (I i)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>n : ℕ<VAR>I : FractionalIdeal R⁰ K<GOAL>FractionalIdeal.count K v (I ^ n) = ↑n * FractionalIdeal.count K v I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>FractionalIdeal.count K v ↑v.asIdeal = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>n : ℕ<GOAL>FractionalIdeal.count K v (↑v.asIdeal ^ n) = ↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>n : ℤ<VAR>I : FractionalIdeal R⁰ K<GOAL>FractionalIdeal.count K v (I ^ (-n)) = -FractionalIdeal.count K v (I ^ n)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<GOAL>FractionalIdeal.count K v I⁻¹ = -FractionalIdeal.count K v I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>n : ℤ<VAR>I : FractionalIdeal R⁰ K<GOAL>FractionalIdeal.count K v (I ^ n) = n * FractionalIdeal.count K v I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>n : ℤ<GOAL>FractionalIdeal.count K v (↑v.asIdeal ^ n) = n
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>w : IsDedekindDomain.HeightOneSpectrum R<VAR>hw : w ≠ v<GOAL>FractionalIdeal.count K v ↑w.asIdeal = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v w : IsDedekindDomain.HeightOneSpectrum R<GOAL>FractionalIdeal.count K v ↑w.asIdeal = if w = v then 1 else 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>exps : IsDedekindDomain.HeightOneSpectrum R → ℤ<GOAL>FractionalIdeal.count K v (∏ᶠ (w : IsDedekindDomain.HeightOneSpectrum R) (_ : w ≠ v), ↑w.asIdeal ^ exps w) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>exps : IsDedekindDomain.HeightOneSpectrum R →₀ ℤ<GOAL>FractionalIdeal.count K v (exps.prod fun x x_1 => ↑x.asIdeal ^ x_1) = exps v
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>exps : IsDedekindDomain.HeightOneSpectrum R → ℤ<VAR>h_exps : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, exps v = 0<GOAL>FractionalIdeal.count K v (∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ exps v) = exps v
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>J : Ideal R<VAR>hJ : J ≠ 0<GOAL>FractionalIdeal.count K v ↑J = ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>J : Ideal R<GOAL>0 ≤ FractionalIdeal.count K v ↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>I J : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>h : I ≤ J<GOAL>FractionalIdeal.count K v J ≤ FractionalIdeal.count K v I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<GOAL>∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ↑v.asIdeal ^ FractionalIdeal.count K v I = I
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>a : R<VAR>J : Ideal R<VAR>haJ : I = FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J<GOAL>∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDedekindDomain R<VAR>I : FractionalIdeal R⁰ K<GOAL>∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite, FractionalIdeal.count K v I = 0
<VAR>R : Type u_1<VAR>Zero R<VAR>Pow R ℕ<VAR>x : R<VAR>n : ℕ<VAR>e : x ^ n = 0<GOAL>IsNilpotent x
<VAR>R : Type u_1<VAR>x : R<VAR>Zero R<VAR>Pow R ℕ<VAR>Subsingleton R<GOAL>IsNilpotent x
<VAR>R : Type u_1<VAR>MonoidWithZero R<GOAL>IsNilpotent 0
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>Nontrivial R<GOAL>¬IsNilpotent 1
<VAR>n : ℕ<VAR>S : Type u_3<VAR>MonoidWithZero S<VAR>x : S<VAR>hx : IsNilpotent x<GOAL>IsNilpotent (x ^ n.succ)
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>x : R<VAR>m : ℕ<VAR>h : IsNilpotent (x ^ m)<GOAL>IsNilpotent x
<VAR>n : ℕ<VAR>S : Type u_3<VAR>MonoidWithZero S<VAR>x : S<VAR>hx : IsNilpotent x<VAR>hn : n ≠ 0<GOAL>IsNilpotent (x ^ n)
<VAR>n : ℕ<VAR>S : Type u_3<VAR>MonoidWithZero S<VAR>x : S<VAR>hn : n ≠ 0<GOAL>IsNilpotent (x ^ n) ↔ IsNilpotent x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>MonoidWithZero R<VAR>MonoidWithZero S<VAR>r : R<VAR>F : Type u_3<VAR>FunLike F R S<VAR>MonoidWithZeroHomClass F R S<VAR>hr : IsNilpotent r<VAR>f : F<GOAL>IsNilpotent (f r)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>MonoidWithZero R<VAR>MonoidWithZero S<VAR>r : R<VAR>F : Type u_3<VAR>FunLike F R S<VAR>MonoidWithZeroHomClass F R S<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>IsNilpotent (f r) ↔ IsNilpotent r
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>r u : R<VAR>hu : IsUnit u<VAR>h_comm : Commute r u<GOAL>IsNilpotent (r * u) ↔ IsNilpotent r
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>r u : R<VAR>hu : IsUnit u<VAR>h_comm : Commute r u<GOAL>IsNilpotent (u * r) ↔ IsNilpotent r
<VAR>R : Type u_1<VAR>x : R<VAR>Zero R<VAR>Pow R ℕ<VAR>Subsingleton R<GOAL>nilpotencyClass x = 0
<VAR>R : Type u_1<VAR>x : R<VAR>Zero R<VAR>Pow R ℕ<VAR>hx : 0 < nilpotencyClass x<GOAL>IsNilpotent x
<VAR>R : Type u_1<VAR>x : R<VAR>Zero R<VAR>Pow R ℕ<VAR>hx : IsNilpotent x<GOAL>x ^ nilpotencyClass x = 0
<VAR>R : Type u_1<VAR>x : R<VAR>MonoidWithZero R<VAR>k : ℕ<GOAL>nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>Nontrivial R<GOAL>nilpotencyClass 0 = 1
<VAR>R : Type u_1<VAR>x : R<VAR>MonoidWithZero R<VAR>Nontrivial R<GOAL>0 < nilpotencyClass x ↔ IsNilpotent x
<VAR>R : Type u_1<VAR>x : R<VAR>MonoidWithZero R<VAR>Nontrivial R<VAR>hx : IsNilpotent x<GOAL>x ^ (nilpotencyClass x - 1) ≠ 0
<VAR>R : Type u_1<VAR>x : R<VAR>MonoidWithZero R<VAR>hx : nilpotencyClass x = 1<GOAL>x = 0
<VAR>R : Type u_1<VAR>x : R<VAR>MonoidWithZero R<VAR>Nontrivial R<GOAL>nilpotencyClass x = 1 ↔ x = 0
<VAR>R : Type u_3<VAR>Zero R<VAR>Pow R ℕ<VAR>self : IsReduced R<VAR>x : R<GOAL>IsNilpotent x → x = 0
<VAR>R : Type u_3<VAR>Zero R<VAR>Pow R ℕ<GOAL>IsReduced R ↔ ∀ (x : R), IsNilpotent x → x = 0
<VAR>R : Type u_1<VAR>x : R<VAR>Zero R<VAR>Pow R ℕ<VAR>IsReduced R<VAR>h : IsNilpotent x<GOAL>x = 0
<VAR>R : Type u_1<VAR>x : R<VAR>MonoidWithZero R<VAR>IsReduced R<GOAL>IsNilpotent x ↔ x = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>MonoidWithZero R<VAR>MonoidWithZero S<VAR>F : Type u_3<VAR>FunLike F R S<VAR>MonoidWithZeroHomClass F R S<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>IsReduced S<GOAL>IsReduced R
<VAR>R : Type u_1<VAR>y : R<VAR>MonoidWithZero R<VAR>k : ℕ<VAR>hk : 1 < k<GOAL>IsRadical y ↔ ∀ (x : R), y ∣ x ^ k → y ∣ x
<VAR>R : Type u_1<VAR>x y : R<VAR>Semiring R<VAR>h_comm : Commute x y<VAR>h : IsNilpotent x<GOAL>IsNilpotent (x * y)
<VAR>R : Type u_1<VAR>x y : R<VAR>Semiring R<VAR>h_comm : Commute x y<VAR>h : IsNilpotent y<GOAL>IsNilpotent (x * y)
<VAR>R : Type u_1<VAR>S : Type u_3<VAR>F : Type u_4<VAR>CommSemiring R<VAR>CommRing S<VAR>FunLike F R S<VAR>RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>(RingHom.ker f).IsRadical ↔ IsReduced S
<VAR>R : Type u_1<VAR>y : R<VAR>CommSemiring R<GOAL>IsRadical y ↔ (Ideal.span {y}).IsRadical
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<GOAL>x ∈ nilradical R ↔ IsNilpotent x
<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>nilradical R = sInf {J | J.IsPrime}
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>x : R<GOAL>IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>J : Ideal R<VAR>H : J.IsPrime<GOAL>nilradical R ≤ J
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>IsReduced R<GOAL>nilradical R = 0
<VAR>R : Type u_1<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<GOAL>IsNilpotent (LinearMap.mulLeft R a) ↔ IsNilpotent a
<VAR>R : Type u_1<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a : A<GOAL>IsNilpotent (LinearMap.mulRight R a) ↔ IsNilpotent a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>M : Type u_4<VAR>Fintype ι<VAR>DecidableEq ι<VAR>AddCommMonoid M<VAR>Module R M<VAR>b : Basis ι R M<VAR>f : M →ₗ[R] M<GOAL>IsNilpotent ((LinearMap.toMatrix b b) f) ↔ IsNilpotent f