ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>x : K<VAR>S : ValuationSubring K<GOAL>x ∈ g • S ↔ ∃ s ∈ S, g • s = x
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>S : ValuationSubring K<VAR>x : K<GOAL>g • x ∈ g • S ↔ x ∈ S
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>S : ValuationSubring K<VAR>x : K<GOAL>x ∈ g • S ↔ g⁻¹ • x ∈ S
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>S : ValuationSubring K<VAR>x : K<GOAL>x ∈ g⁻¹ • S ↔ g • x ∈ S
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>S T : ValuationSubring K<GOAL>g • S ≤ g • T ↔ S ≤ T
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>S T : ValuationSubring K<GOAL>g • S ≤ T ↔ S ≤ g⁻¹ • T
<VAR>K : Type u<VAR>Field K<VAR>G : Type u_1<VAR>Group G<VAR>MulSemiringAction G K<VAR>g : G<VAR>S T : ValuationSubring K<GOAL>S ≤ g • T ↔ g⁻¹ • S ≤ T
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>Field L<VAR>A : ValuationSubring L<VAR>f : K →+* L<GOAL>↑(A.comap f) = ⇑f ⁻¹' ↑A
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>Field L<VAR>A : ValuationSubring L<VAR>f : K →+* L<VAR>x : K<GOAL>x ∈ A.comap f ↔ f x ∈ A
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>J : Type u_2<VAR>Field L<VAR>Field J<VAR>A : ValuationSubring J<VAR>g : L →+* J<VAR>f : K →+* L<GOAL>(A.comap g).comap f = A.comap (g.comp f)
<VAR>K : Type u<VAR>Field K<VAR>Γ : Type u_1<VAR>LinearOrderedCommGroupWithZero Γ<VAR>v : Valuation K Γ<VAR>x : Kˣ<GOAL>x ∈ v.valuationSubring.unitGroup ↔ v ↑x = 1
<VAR>α : Type u<GOAL>Function.Injective FreeRing.of
<VAR>α : Type u<VAR>C : FreeRing α → Prop<VAR>z : FreeRing α<VAR>hn1 : C (-1)<VAR>hb : ∀ (b : α), C (FreeRing.of b)<VAR>ha : ∀ (x y : FreeRing α), C x → C y → C (x + y)<VAR>hm : ∀ (x y : FreeRing α), C x → C y → C (x * y)<GOAL>C z
<VAR>α : Type u<VAR>R : Type v<VAR>Ring R<VAR>f : α → R<VAR>x : α<GOAL>(FreeRing.lift f) (FreeRing.of x) = f x
<VAR>α : Type u<VAR>R : Type v<VAR>Ring R<VAR>f : FreeRing α →+* R<GOAL>FreeRing.lift (⇑f ∘ FreeRing.of) = f
<VAR>α : Type u<VAR>R : Type v<VAR>Ring R<VAR>f g : FreeRing α →+* R<VAR>h : ∀ (x : α), f (FreeRing.of x) = g (FreeRing.of x)<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>(FreeRing.map f) (FreeRing.of x) = FreeRing.of (f x)
<VAR>α : Type u_2<VAR>CommMonoidWithZero α<VAR>self : WfDvdMonoid α<GOAL>WellFounded DvdNotUnit
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<GOAL>WfDvdMonoid (Associates α) → WfDvdMonoid α
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>WfDvdMonoid α<GOAL>WellFounded fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>a : α<VAR>ha : ¬IsUnit a<VAR>ha0 : a ≠ 0<GOAL>∃ i, Irreducible i ∧ i ∣ a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>hu : ∀ (u : α), IsUnit u → P u<VAR>hi : ∀ (a i : α), a ≠ 0 → Irreducible i → P a → P (i * a)<GOAL>P a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>a : α<GOAL>a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>a : α<VAR>hn0 : a ≠ 0<GOAL>¬IsUnit a ↔ ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>x y : α<VAR>nonzero : ¬(x = 0 ∧ y = 0)<VAR>H : ∀ (z : α), Irreducible z → z ∣ x → ¬z ∣ y<GOAL>IsRelPrime x y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>h : WellFounded fun x x_1 => x < x_1<GOAL>WfDvdMonoid α
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<GOAL>WfDvdMonoid α ↔ WellFounded fun x x_1 => x < x_1
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>a₀ x : α<VAR>h : a₀ ≠ 0<VAR>hx : ¬IsUnit x<GOAL>∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
<VAR>α : Type u_1<VAR>CommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>a₀ x : α<VAR>h : a₀ ≠ 0<VAR>hx : Irreducible x<GOAL>∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>a b : α<VAR>ha : ¬IsUnit a<VAR>hb : b ≠ 0<GOAL>multiplicity.Finite a b
<VAR>α : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>self : UniqueFactorizationMonoid α<VAR>a : α<GOAL>Irreducible a ↔ Prime a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>WfDvdMonoid α<VAR>DecompositionMonoid α<GOAL>UniqueFactorizationMonoid α
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : α<GOAL>a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<GOAL>(∃ p, Prime p) ↔ ∃ x, x ≠ 0 ∧ ¬IsUnit x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>P : α → Prop<VAR>a : α<VAR>h₁ : P 0<VAR>h₂ : ∀ (x : α), IsUnit x → P x<VAR>h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)<GOAL>P a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>f g : Multiset α<GOAL>(∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>f g : Multiset α<VAR>hf : ∀ x ∈ f, Irreducible x<VAR>hg : ∀ x ∈ g, Irreducible x<VAR>h : f.prod ~ᵤ g.prod<GOAL>Multiset.Rel Associated f g
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a : α<VAR>f : Multiset α<VAR>ha : Irreducible a<VAR>pfa : (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<GOAL>∃ p, a ~ᵤ p ∧ f = {p}
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<GOAL>WfDvdMonoid α
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<VAR>p : α<GOAL>Irreducible p ↔ Prime p
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a<GOAL>UniqueFactorizationMonoid α
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<GOAL>UniqueFactorizationMonoid α ↔ ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>CancelCommMonoidWithZero β<VAR>e : α ≃* β<VAR>hα : UniqueFactorizationMonoid α<GOAL>UniqueFactorizationMonoid β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>CancelCommMonoidWithZero α<VAR>CancelCommMonoidWithZero β<VAR>e : α ≃* β<GOAL>UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g<VAR>p : α<GOAL>Irreducible p ↔ Prime p
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g<GOAL>UniqueFactorizationMonoid α
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<GOAL>(UniqueFactorizationMonoid.factors a).prod ~ᵤ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<GOAL>UniqueFactorizationMonoid.factors 0 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>p a : α<VAR>h : p ∈ UniqueFactorizationMonoid.factors a<GOAL>a ≠ 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>p a : α<VAR>h : p ∈ UniqueFactorizationMonoid.factors a<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>x : α<VAR>hx : x ∈ UniqueFactorizationMonoid.factors a<GOAL>Prime x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>x : α<GOAL>x ∈ UniqueFactorizationMonoid.factors a → Irreducible x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<GOAL>UniqueFactorizationMonoid.factors 1 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<GOAL>p ∣ a → ∃ q ∈ UniqueFactorizationMonoid.factors a, p ~ᵤ q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<VAR>h : ¬IsUnit x<GOAL>∃ p, p ∈ UniqueFactorizationMonoid.factors x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>Multiset.Rel Associated (UniqueFactorizationMonoid.factors (x * y)) (UniqueFactorizationMonoid.factors x + UniqueFactorizationMonoid.factors y)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>x : α<VAR>n : ℕ<GOAL>Multiset.Rel Associated (UniqueFactorizationMonoid.factors (x ^ n)) (n • UniqueFactorizationMonoid.factors x)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<GOAL>0 < UniqueFactorizationMonoid.factors x ↔ ¬IsUnit x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq α<VAR>x : α<VAR>hx : x ≠ 0<GOAL>∏ p ∈ (UniqueFactorizationMonoid.factors x).toFinset, p ^ Multiset.count p (UniqueFactorizationMonoid.factors x) ~ᵤ x
<VAR>M : Type u_2<VAR>CancelCommMonoidWithZero M<VAR>UniqueFactorizationMonoid M<VAR>Unique Mˣ<VAR>x : M<GOAL>UniqueFactorizationMonoid.factors x = UniqueFactorizationMonoid.normalizedFactors x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>ane0 : a ≠ 0<GOAL>(UniqueFactorizationMonoid.normalizedFactors a).prod ~ᵤ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>x : α<GOAL>x ∈ UniqueFactorizationMonoid.normalizedFactors a → Prime x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>x : α<GOAL>x ∈ UniqueFactorizationMonoid.normalizedFactors a → Irreducible x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>x : α<GOAL>x ∈ UniqueFactorizationMonoid.normalizedFactors a → normalize x = x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>ha : Irreducible a<GOAL>UniqueFactorizationMonoid.normalizedFactors a = {normalize a}
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a p : α<GOAL>p ∈ UniqueFactorizationMonoid.normalizedFactors a → ∀ q ∈ UniqueFactorizationMonoid.normalizedFactors a, p ∣ q → p = q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<GOAL>p ∣ a → ∃ q ∈ UniqueFactorizationMonoid.normalizedFactors a, p ~ᵤ q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<VAR>h : ¬IsUnit x<GOAL>∃ p, p ∈ UniqueFactorizationMonoid.normalizedFactors x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<GOAL>UniqueFactorizationMonoid.normalizedFactors 0 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<GOAL>UniqueFactorizationMonoid.normalizedFactors 1 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>UniqueFactorizationMonoid.normalizedFactors (x * y) = UniqueFactorizationMonoid.normalizedFactors x + UniqueFactorizationMonoid.normalizedFactors y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>x : α<VAR>n : ℕ<GOAL>UniqueFactorizationMonoid.normalizedFactors (x ^ n) = n • UniqueFactorizationMonoid.normalizedFactors x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>p : α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>UniqueFactorizationMonoid.normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>s : Multiset α<VAR>hs : ∀ a ∈ s, Irreducible a<GOAL>UniqueFactorizationMonoid.normalizedFactors s.prod = Multiset.map (⇑normalize) s
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x ∣ y ↔ UniqueFactorizationMonoid.normalizedFactors x ≤ UniqueFactorizationMonoid.normalizedFactors y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x ~ᵤ y ↔ UniqueFactorizationMonoid.normalizedFactors x = UniqueFactorizationMonoid.normalizedFactors y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>x : α<GOAL>0 ∉ UniqueFactorizationMonoid.normalizedFactors x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a p : α<VAR>H : p ∈ UniqueFactorizationMonoid.normalizedFactors a<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>Unique αˣ<VAR>p x : α<VAR>hx : x ≠ 0<GOAL>p ∈ UniqueFactorizationMonoid.normalizedFactors x ↔ Prime p ∧ p ∣ x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>p r : α<VAR>h : ∀ {m : α}, m ∈ UniqueFactorizationMonoid.normalizedFactors r → m = p<VAR>hr : r ≠ 0<GOAL>∃ i, p ^ i ~ᵤ r
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>Unique αˣ<VAR>m : Multiset α<VAR>h : ∀ p ∈ m, Prime p<GOAL>UniqueFactorizationMonoid.normalizedFactors m.prod = m
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>a b c : α<VAR>ha : a ∈ UniqueFactorizationMonoid.normalizedFactors c<VAR>hb : b ∈ UniqueFactorizationMonoid.normalizedFactors c<VAR>h : a ~ᵤ b<GOAL>a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>x : α<VAR>hx : x ≠ 0<GOAL>0 < UniqueFactorizationMonoid.normalizedFactors x ↔ ¬IsUnit x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>x y : α<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>DvdNotUnit x y ↔ UniqueFactorizationMonoid.normalizedFactors x < UniqueFactorizationMonoid.normalizedFactors y
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>NormalizationMonoid α<VAR>UniqueFactorizationMonoid α<VAR>s : Multiset α<VAR>hs : 0 ∉ s<GOAL>UniqueFactorizationMonoid.normalizedFactors s.prod = (Multiset.map UniqueFactorizationMonoid.normalizedFactors s).sum
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>a b : R<VAR>ha : a ≠ 0<GOAL>IsRelPrime a b ↔ ∀ ⦃d : R⦄, d ∣ a → d ∣ b → ¬Prime d
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>h : ∀ ⦃d : R⦄, d ∣ a → d ∣ c → ¬Prime d<GOAL>a ∣ b * c → a ∣ b
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>a b c : R<VAR>ha : a ≠ 0<VAR>no_factors : ∀ {d : R}, d ∣ a → d ∣ b → ¬Prime d<GOAL>a ∣ b * c → a ∣ c
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>a : R<GOAL>a ≠ 0 → ∀ (b : R), ∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>a b : R<VAR>hb : b ≠ 0<GOAL>∃ a' b' c', IsRelPrime a' b' ∧ c' * a' = a ∧ c' * b' = b
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>a : R<VAR>ha0 : a ≠ 0<VAR>ha1 : ¬IsUnit a<GOAL>Function.Injective fun x => a ^ x
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>a : R<VAR>ha0 : a ≠ 0<VAR>ha1 : ¬IsUnit a<VAR>i j : ℕ<GOAL>a ^ i = a ^ j ↔ i = j
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>NormalizationMonoid R<VAR>DecidableRel Dvd.dvd<VAR>a b : R<VAR>n : ℕ<VAR>ha : Irreducible a<VAR>hb : b ≠ 0<GOAL>↑n ≤ multiplicity a b ↔ Multiset.replicate n (normalize a) ≤ UniqueFactorizationMonoid.normalizedFactors b
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>NormalizationMonoid R<VAR>DecidableRel Dvd.dvd<VAR>DecidableEq R<VAR>a b : R<VAR>ha : Irreducible a<VAR>hb : b ≠ 0<GOAL>multiplicity a b = ↑(Multiset.count (normalize a) (UniqueFactorizationMonoid.normalizedFactors b))
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>NormalizationMonoid R<VAR>DecidableEq R<VAR>p x : R<VAR>hp : Irreducible p<VAR>hnorm : normalize p = p<VAR>n : ℕ<VAR>hle : p ^ n ∣ x<VAR>hlt : ¬p ^ (n + 1) ∣ x<GOAL>Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>NormalizationMonoid R<VAR>DecidableEq R<VAR>p x : R<VAR>hp : p = 0 ∨ Irreducible p<VAR>hnorm : normalize p = p<VAR>n : ℕ<VAR>hle : p ^ n ∣ x<VAR>hlt : ¬p ^ (n + 1) ∣ x<GOAL>Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
<VAR>R : Type u_2<VAR>CancelCommMonoidWithZero R<VAR>UniqueFactorizationMonoid R<VAR>a₀ x : R<VAR>h : a₀ ≠ 0<VAR>hx : Irreducible x<GOAL>∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq α<VAR>s : Finset α<VAR>i : α → ℕ<VAR>p : α<VAR>hps : p ∉ s<VAR>is_prime : ∀ q ∈ insert p s, Prime q<VAR>is_coprime : ∀ q ∈ insert p s, ∀ q' ∈ insert p s, q ∣ q' → q = q'<GOAL>IsRelPrime (p ^ i p) (∏ p' ∈ s, p' ^ i p')
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>P : α → Prop<VAR>s : Finset α<VAR>i : α → ℕ<VAR>is_prime : ∀ p ∈ s, Prime p<VAR>is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<GOAL>P (∏ p ∈ s, p ^ i p)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>P : α → Prop<VAR>a : α<VAR>h0 : P 0<VAR>h1 : ∀ {x : α}, IsUnit x → P x<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → P (p ^ i)<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)<GOAL>P a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero β<VAR>f : α → β<VAR>s : Finset α<VAR>i j : α → ℕ<VAR>is_prime : ∀ p ∈ s, Prime p<VAR>is_coprime : ∀ p ∈ s, ∀ q ∈ s, p ∣ q → p = q<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<GOAL>f (∏ p ∈ s, p ^ (i p + j p)) = f (∏ p ∈ s, p ^ i p) * f (∏ p ∈ s, p ^ j p)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>CancelCommMonoidWithZero β<VAR>f : α → β<VAR>a b : α<VAR>h0 : f 0 = 0<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<GOAL>f (a * b) = f a * f b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b : Multiset { a // Irreducible a }<GOAL>↑(a + b) = ↑a + ↑b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableEq (Associates α)<VAR>a b : Associates.FactorSet α<GOAL>a ⊔ b + a ⊓ b = a + b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<GOAL>⊤.prod = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>s : Multiset { a // Irreducible a }<GOAL>Associates.FactorSet.prod ↑s = (Multiset.map Subtype.val s).prod
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b : Associates.FactorSet α<GOAL>(a + b).prod = a.prod * b.prod
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>a b : Associates.FactorSet α<GOAL>a ≤ b → a.prod ≤ b.prod
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>Nontrivial α<VAR>p : Associates.FactorSet α<GOAL>p.prod = 0 ↔ p = ⊤
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>s : Multiset { a // Irreducible a }<GOAL>p.count ↑s = Multiset.count ⟨p, hp⟩ s
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count 0 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>p : Associates α<VAR>hp : ¬Irreducible p<GOAL>p.count = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : Associates α<VAR>s : Associates.FactorSet α<GOAL>p.FactorSetMem s = (p ∈ s)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p ∈ ⊤
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>l : Multiset { a // Irreducible a }<GOAL>p ∈ ↑l ↔ ⟨p, hp⟩ ∈ l
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : Associates α<VAR>hp : ¬Irreducible p<VAR>s : Associates.FactorSet α<GOAL>p ∉ s
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>p : Associates α<VAR>s : Associates.FactorSet α<VAR>h : p ∈ s<GOAL>Irreducible p
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>p q : Multiset (Associates α)<GOAL>(∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>p q : Associates.FactorSet α<VAR>h : p.prod = q.prod<GOAL>p = q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>p q : Multiset (Associates α)<VAR>hp : ∀ a ∈ p, Irreducible a<VAR>hq : ∀ a ∈ q, Irreducible a<GOAL>p.prod ≤ q.prod ↔ p ≤ q
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : α<GOAL>Multiset.map Subtype.val (Associates.factors' a) = Multiset.map Associates.mk (UniqueFactorizationMonoid.factors a)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b : α<VAR>h : a ~ᵤ b<GOAL>Associates.factors' a = Associates.factors' b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<GOAL>Associates.factors 0 = ⊤
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>h : a ≠ 0<GOAL>(Associates.mk a).factors = ↑(Associates.factors' a)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : Associates α<GOAL>a.factors.prod = a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>s : Associates.FactorSet α<GOAL>s.prod.factors = s
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Subsingleton α<VAR>a : Associates α<GOAL>a.factors = ⊤
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : Associates α<GOAL>a.factors = ⊤ ↔ a = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : Associates α<GOAL>(∃ s, a.factors = ↑s) ↔ a ≠ 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b : Associates α<VAR>h : a.factors = b.factors<GOAL>a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>a b : Associates.FactorSet α<VAR>h : a.prod = b.prod<GOAL>a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b : Associates α<GOAL>(a * b).factors = a.factors + b.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b : Associates α<GOAL>a ≤ b → a.factors ≤ b.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b : Associates α<GOAL>a.factors ≤ b.factors ↔ a ≤ b