ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors<GOAL>a.factors = b.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>a b : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : ∀ (p : Associates α), Irreducible p → p.count a.factors = p.count b.factors<GOAL>a = b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>a b p : Associates α<VAR>hb : b ≠ 0<VAR>hp : Irreducible p<VAR>h : a.factors ≤ b.factors<GOAL>p.count a.factors ≤ p.count b.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>a b p : Associates α<VAR>hb : b ≠ 0<VAR>hp : Irreducible p<VAR>h : a ≤ b<GOAL>p.count a.factors ≤ p.count b.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>a b : Associates.FactorSet α<GOAL>a.prod ≤ b.prod ↔ a ≤ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b : Associates α<GOAL>(a ⊔ b) * (a ⊓ b) = a * b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hm : p ∈ a.factors<GOAL>p ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a : α<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hz : a ≠ 0<VAR>h_mem : ⟨p, hp⟩ ∈ Associates.factors' a<GOAL>p ∣ Associates.mk a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<GOAL>⟨Associates.mk p, ⋯⟩ ∈ Associates.factors' a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<GOAL>⟨Associates.mk p, ⋯⟩ ∈ Associates.factors' a ↔ p ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<VAR>hd : p ∣ a<GOAL>Associates.mk p ∈ (Associates.mk a).factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<GOAL>Associates.mk p ∈ (Associates.mk a).factors ↔ p ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : Associates.mk a ⊓ Associates.mk b ≠ 1<GOAL>∃ p, Prime p ∧ p ∣ a ∧ p ∣ b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b : α<VAR>ha0 : a ≠ 0<VAR>hb0 : b ≠ 0<GOAL>Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.factors = ↑{⟨p, hp⟩}
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>(p ^ k).factors = ↑(Multiset.replicate k ⟨p, hp⟩)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq (Associates α)<VAR>m p : Associates α<VAR>h₁ : m ≠ 0<VAR>h₂ : Irreducible p<VAR>k : ℕ<GOAL>p ^ k ≤ m ↔ k ≤ Associates.bcount ⟨p, h₂⟩ m.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>m p : Associates α<VAR>h₁ : m ≠ 0<VAR>h₂ : Irreducible p<VAR>k : ℕ<GOAL>p ^ k ≤ m ↔ k ≤ p.count m.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>m p : Associates α<VAR>h0 : m ≠ 0<VAR>hp : Irreducible p<GOAL>p.count m.factors ≠ 0 → p ≤ m
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>DecidableEq (Associates α)<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>a p : α<VAR>ha0 : a ≠ 0<VAR>hp : Irreducible p<GOAL>(Associates.mk p).count (Associates.mk a).factors ≠ 0 ↔ p ∣ a
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>Nontrivial α<VAR>DecidableEq (Associates α)<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count p.factors = 1
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>p q : Associates α<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>h : p ≠ q<GOAL>p.count q.factors = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count (a * b).factors = p.count a.factors + p.count b.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>b : Associates α<VAR>hb : b ≠ 0<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>p : Associates α<VAR>hp : Irreducible p<GOAL>p.count a.factors = 0 ∨ p.count b.factors = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<GOAL>p.count a.factors = 0 ∨ p.count a.factors = p.count (a * b).factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>a b p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<GOAL>p.count (a * b).factors = p.count a.factors ∨ p.count (a * b).factors = p.count b.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>a b : Associates α<VAR>hb : b ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>k : ℕ<VAR>habk : k ∣ p.count (a * b).factors<GOAL>k ∣ p.count a.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<GOAL>Associates.factors 1 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>Nontrivial α<VAR>a : Associates α<VAR>k : ℕ<GOAL>(a ^ k).factors = k • a.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>Nontrivial α<VAR>DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>p.count (a ^ k).factors = k * p.count a.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>Nontrivial α<VAR>DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>p : Associates α<VAR>hp : Irreducible p<VAR>k : ℕ<GOAL>k ∣ p.count (a ^ k).factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>a : Associates α<VAR>ha : a ≠ 0<VAR>k : ℕ<VAR>hk : ∀ (p : Associates α), Irreducible p → k ∣ p.count a.factors<GOAL>∃ b, a = b ^ k
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>p a : Associates α<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>a = p ^ p.count a.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>(p : Associates α) → Decidable (Irreducible p)<VAR>DecidableEq (Associates α)<VAR>a p : Associates α<VAR>hp : Irreducible p<VAR>(n : ℕ) → Decidable (a ∣ p ^ n)<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>Nat.find ⋯ = p.count a.factors
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a b c : Associates α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>hab : ∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d<VAR>k : ℕ<VAR>h : a * b = c ^ k<GOAL>∃ d, a = d ^ k
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>a p : Associates α<VAR>hp : Irreducible p<VAR>(n : ℕ) → Decidable (a ∣ p ^ n)<VAR>n : ℕ<VAR>h : a ∣ p ^ n<GOAL>a = p ^ Nat.find ⋯
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>NormalizationMonoid α<VAR>DecidableEq α<VAR>n p : α<GOAL>(factorization n) p = Multiset.count p (UniqueFactorizationMonoid.normalizedFactors n)
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>NormalizationMonoid α<VAR>DecidableEq α<GOAL>factorization 0 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>NormalizationMonoid α<VAR>DecidableEq α<GOAL>factorization 1 = 0
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>NormalizationMonoid α<VAR>DecidableEq α<VAR>n : α<GOAL>(factorization n).support = (UniqueFactorizationMonoid.normalizedFactors n).toFinset
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>NormalizationMonoid α<VAR>DecidableEq α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>factorization (a * b) = factorization a + factorization b
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>NormalizationMonoid α<VAR>DecidableEq α<VAR>x : α<VAR>n : ℕ<GOAL>factorization (x ^ n) = n • factorization x
<VAR>α : Type u_1<VAR>CancelCommMonoidWithZero α<VAR>UniqueFactorizationMonoid α<VAR>NormalizationMonoid α<VAR>DecidableEq α<VAR>a b : α<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : factorization a = factorization b<GOAL>a ~ᵤ b
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>IsDomain R<VAR>UniqueFactorizationMonoid R<VAR>I : Ideal R<VAR>hI₂ : I.IsPrime<VAR>hI : I ≠ ⊥<GOAL>∃ x ∈ I, Prime x
<VAR>n : ℕ<GOAL>UniqueFactorizationMonoid.normalizedFactors n = ↑n.primeFactorsList
<VAR>s : Multiset ℕ<VAR>h : ∀ x ∈ s, Irreducible x<GOAL>UniqueFactorizationMonoid.normalizedFactors s.prod = s
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>(MvPolynomial.bind₁ (wittStructureRat p Φ)) (W_ ℚ n) = (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (W_ ℚ n)) Φ
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<GOAL>∃! φ, ∀ (n : ℕ), (MvPolynomial.bind₁ φ) (W_ ℚ n) = (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (W_ ℚ n)) Φ
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>wittStructureRat p Φ n * MvPolynomial.C (↑p ^ n) = (MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) (W_ ℚ n)) Φ - ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>wittStructureRat p Φ n = MvPolynomial.C (1 / ↑p ^ n) * ((MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) (W_ ℚ n)) Φ - ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * wittStructureRat p Φ i ^ p ^ (n - i))
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) m<GOAL>(MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) ((MvPolynomial.expand p) (W_ ℤ n))) Φ = (MvPolynomial.bind₁ fun i => (MvPolynomial.expand p) (wittStructureInt p Φ i)) (W_ ℤ n)
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<VAR>IH : ∀ m < n, (MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ m) = wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) m<GOAL>MvPolynomial.C ↑(p ^ n) ∣ (MvPolynomial.bind₁ fun b => (MvPolynomial.rename fun i => (b, i)) (W_ ℤ n)) Φ - ∑ i ∈ Finset.range n, MvPolynomial.C (↑p ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (wittStructureInt p Φ n) = wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) n
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(MvPolynomial.bind₁ (wittStructureInt p Φ)) (W_ ℤ n) = (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (W_ ℤ n)) Φ
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>φ : ℕ → MvPolynomial (idx × ℕ) ℤ<VAR>h : ∀ (n : ℕ), (MvPolynomial.bind₁ φ) (W_ ℤ n) = (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (W_ ℤ n)) Φ<GOAL>φ = wittStructureInt p Φ
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<GOAL>∃! φ, ∀ (n : ℕ), (MvPolynomial.bind₁ φ) (W_ ℤ n) = (MvPolynomial.bind₁ fun i => (MvPolynomial.rename (Prod.mk i)) (W_ ℤ n)) Φ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(MvPolynomial.aeval fun i => (MvPolynomial.map (Int.castRingHom R)) (wittStructureInt p Φ i)) (W_ ℤ n) = (MvPolynomial.aeval fun i => (MvPolynomial.rename (Prod.mk i)) (W_ R n)) Φ
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>σ : Type u_3<VAR>Φ : MvPolynomial idx ℤ<VAR>f : idx → σ<VAR>n : ℕ<GOAL>wittStructureInt p ((MvPolynomial.rename f) Φ) n = (MvPolynomial.rename (Prod.map f id)) (wittStructureInt p Φ n)
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<GOAL>MvPolynomial.constantCoeff (wittStructureRat p Φ 0) = MvPolynomial.constantCoeff Φ
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℚ<VAR>h : MvPolynomial.constantCoeff Φ = 0<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (wittStructureRat p Φ n) = 0
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<GOAL>MvPolynomial.constantCoeff (wittStructureInt p Φ 0) = MvPolynomial.constantCoeff Φ
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Φ : MvPolynomial idx ℤ<VAR>h : MvPolynomial.constantCoeff Φ = 0<VAR>n : ℕ<GOAL>MvPolynomial.constantCoeff (wittStructureInt p Φ n) = 0
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<GOAL>(wittStructureRat p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>idx : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>Fintype idx<VAR>Φ : MvPolynomial idx ℤ<VAR>n : ℕ<GOAL>(wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.PreSubmersivePresentation R S<GOAL>Function.Injective self.map
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.PreSubmersivePresentation R S<GOAL>Finite self.rels
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.PreSubmersivePresentation R S<VAR>P.IsFinite<GOAL>Nat.card P.rels ≤ Nat.card P.vars
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.PreSubmersivePresentation R S<VAR>Fintype P.rels<VAR>DecidableEq P.rels<GOAL>P.jacobian = (algebraMap P.Ring S) P.jacobiMatrix.det
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.PreSubmersivePresentation R S<VAR>Fintype P.rels<VAR>DecidableEq P.rels<VAR>i j : P.rels<GOAL>P.jacobiMatrix i j = (MvPolynomial.pderiv (P.map i)) (P.relation j)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.SubmersivePresentation R S<GOAL>IsUnit self.jacobian
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.SubmersivePresentation R S<GOAL>self.IsFinite
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.IsStandardSmooth R S<GOAL>Nonempty (Algebra.SubmersivePresentation R S)
<VAR>n : ℕ<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.IsStandardSmoothOfRelativeDimension n R S<GOAL>∃ P, P.dimension = n
<VAR>n : ℕ<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.IsStandardSmoothOfRelativeDimension n R S<GOAL>Algebra.IsStandardSmooth R S
<VAR>n : ℕ<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : RingHom.IsStandardSmoothOfRelativeDimension n f<GOAL>f.IsStandardSmooth
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(MvPolynomial.bind₁ (WittVector.frobeniusPolyRat p)) (wittPolynomial p ℚ n) = wittPolynomial p ℚ (n + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>WittVector.frobeniusPolyAux p n = MvPolynomial.X (n + 1) - ∑ i ∈ Finset.range n, ∑ j ∈ Finset.range (p ^ (n - i)), (MvPolynomial.X i ^ p) ^ (p ^ (n - i) - (j + 1)) * WittVector.frobeniusPolyAux p i ^ (j + 1) * MvPolynomial.C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩) * p ^ (j - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n j : ℕ<VAR>hj : j < p ^ n<GOAL>p ^ (n - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩) ∣ (p ^ n).choose (j + 1)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n i j : ℕ<VAR>hi : i ≤ n<VAR>hj : j < p ^ (n - i)<GOAL>j - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩ + n = i + j + (n - i - WittVector.pnat_multiplicity p ⟨j + 1, ⋯⟩)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom ℚ)) (WittVector.frobeniusPoly p n) = WittVector.frobeniusPolyRat p n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(MvPolynomial.map (Int.castRingHom (ZMod p))) (WittVector.frobeniusPoly p n) = MvPolynomial.X n ^ p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>(MvPolynomial.bind₁ (WittVector.frobeniusPoly p)) (wittPolynomial p ℤ n) = wittPolynomial p ℤ (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>x.frobeniusFun.coeff n = (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>n : ℕ<VAR>x : WittVector p R<GOAL>(WittVector.ghostComponent n) x.frobeniusFun = (WittVector.ghostComponent (n + 1)) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>(WittVector.frobenius x).coeff n = (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>n : ℕ<VAR>x : WittVector p R<GOAL>(WittVector.ghostComponent n) (WittVector.frobenius x) = (WittVector.ghostComponent (n + 1)) x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>x : WittVector p R<VAR>n : ℕ<GOAL>(WittVector.frobenius x).coeff n = x.coeff n ^ p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<GOAL>WittVector.frobenius = WittVector.map (frobenius R p)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : WittVector p (ZMod p)<GOAL>WittVector.frobenius x = x
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>PerfectRing R p<GOAL>⇑(WittVector.frobeniusEquiv p R) = ⇑WittVector.frobenius
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>PerfectRing R p<GOAL>⇑(WittVector.frobeniusEquiv p R).symm = ⇑(WittVector.map ↑(frobeniusEquiv R p).symm)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>CommRing R<VAR>CharP R p<VAR>PerfectRing R p<GOAL>Function.Bijective ⇑WittVector.frobenius
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ ψ : MvPowerSeries σ R<VAR>h : ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ<GOAL>φ = ψ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ ψ : MvPowerSeries σ R<GOAL>φ = ψ ↔ ∀ (n : σ →₀ ℕ), (MvPowerSeries.coeff R n) φ = (MvPowerSeries.coeff R n) ψ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>DecidableEq σ<VAR>n : σ →₀ ℕ<GOAL>MvPowerSeries.monomial R n = LinearMap.stdBasis R (fun x => R) n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>DecidableEq σ<VAR>m n : σ →₀ ℕ<VAR>a : R<GOAL>(MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) = if m = n then a else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>n : σ →₀ ℕ<VAR>a : R<GOAL>(MvPowerSeries.coeff R n) ((MvPowerSeries.monomial R n) a) = a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>m n : σ →₀ ℕ<VAR>h : m ≠ n<VAR>a : R<GOAL>(MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>m n : σ →₀ ℕ<VAR>a : R<VAR>h : (MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a) ≠ 0<GOAL>m = n
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>n : σ →₀ ℕ<GOAL>MvPowerSeries.coeff R n ∘ₗ MvPowerSeries.monomial R n = LinearMap.id
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>n : σ →₀ ℕ<GOAL>(MvPowerSeries.coeff R n) 0 = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>n : σ →₀ ℕ<VAR>DecidableEq σ<GOAL>(MvPowerSeries.coeff R n) 1 = if n = 0 then 1 else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<GOAL>(MvPowerSeries.coeff R 0) 1 = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<GOAL>(MvPowerSeries.monomial R 0) 1 = 1
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>n : σ →₀ ℕ<VAR>φ ψ : MvPowerSeries σ R<VAR>DecidableEq σ<GOAL>(MvPowerSeries.coeff R n) (φ * ψ) = ∑ p ∈ Finset.antidiagonal n, (MvPowerSeries.coeff R p.1) φ * (MvPowerSeries.coeff R p.2) ψ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<GOAL>0 * φ = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<GOAL>φ * 0 = 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>a : R<GOAL>(MvPowerSeries.coeff R m) ((MvPowerSeries.monomial R n) a * φ) = if n ≤ m then a * (MvPowerSeries.coeff R (m - n)) φ else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>a : R<GOAL>(MvPowerSeries.coeff R m) (φ * (MvPowerSeries.monomial R n) a) = if n ≤ m then (MvPowerSeries.coeff R (m - n)) φ * a else 0
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>a : R<GOAL>(MvPowerSeries.coeff R (m + n)) ((MvPowerSeries.monomial R m) a * φ) = a * (MvPowerSeries.coeff R n) φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>m n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>a : R<GOAL>(MvPowerSeries.coeff R (m + n)) (φ * (MvPowerSeries.monomial R n) a) = (MvPowerSeries.coeff R m) φ * a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<VAR>a : R<VAR>n : σ →₀ ℕ<GOAL>Commute φ ((MvPowerSeries.monomial R n) a) ↔ ∀ (m : σ →₀ ℕ), Commute ((MvPowerSeries.coeff R m) φ) a
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<GOAL>1 * φ = φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ : MvPowerSeries σ R<GOAL>φ * 1 = φ
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ₁ φ₂ φ₃ : MvPowerSeries σ R<GOAL>φ₁ * (φ₂ + φ₃) = φ₁ * φ₂ + φ₁ * φ₃
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ₁ φ₂ φ₃ : MvPowerSeries σ R<GOAL>(φ₁ + φ₂) * φ₃ = φ₁ * φ₃ + φ₂ * φ₃
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>Semiring R<VAR>φ₁ φ₂ φ₃ : MvPowerSeries σ R<GOAL>φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)