ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>p a b : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>a ≠ 0 → b ≠ 0 → padicValNat p (a * b) = padicValNat p a + padicValNat p b
<VAR>p b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>dvd : p ∣ b<GOAL>padicValNat p (b / p) = padicValNat p b - 1
<VAR>p a : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>padicValNat p (a ^ n) = n * padicValNat p a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>padicValNat p (p ^ n) = n
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>m : ℕ<VAR>cpm : p.Coprime m<VAR>b : ℕ<VAR>dvd : m ∣ b<GOAL>padicValNat p (b / m) = padicValNat p b
<VAR>p : ℕ<VAR>n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℕ<GOAL>p ^ n ∣ a ↔ a = 0 ∨ n ≤ padicValNat p a
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq : Fact (Nat.Prime q)<VAR>neq : p ≠ q<GOAL>padicValNat p q = 0
<VAR>p q : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hq : Fact (Nat.Prime q)<VAR>n : ℕ<VAR>neq : p ≠ q<GOAL>padicValNat p (q ^ n) = 0
<VAR>p : ℕ<VAR>n : ℕ<GOAL>padicValNat p n ≤ Nat.log p n
<VAR>p n : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hn : 0 < n<GOAL>Nat.log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1)
<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>Nat.log 2 n ≠ padicValNat 2 (n + 1)
<VAR>n : ℕ<GOAL>max (Nat.log 2 n) (padicValNat 2 (n + 1)) = Nat.log 2 (n + 1)
<VAR>p n : ℕ<VAR>hn : n ≠ 0<GOAL>Finset.image (fun x => p ^ x) (Finset.range (padicValNat p n + 1)) ⊆ n.divisors
<VAR>p : ℕ<VAR>n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>padicValNat p (p * n)! = padicValNat p n ! + n
<VAR>p m k : ℕ<VAR>hm : m ∈ Set.Ioo (p * k) (p * (k + 1))<GOAL>padicValNat p m = 0
<VAR>p n : ℕ<VAR>m : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : n < p<GOAL>padicValNat p (p * m + n)! = padicValNat p (p * m)!
<VAR>p : ℕ<VAR>n : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>padicValNat p (p * (n / p))! = padicValNat p n !
<VAR>p n b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hnb : Nat.log p n < b<GOAL>padicValNat p n ! = ∑ i ∈ Finset.Ico 1 b, n / p ^ i
<VAR>p n k b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hkn : k ≤ n<VAR>hnb : Nat.log p n < b<GOAL>padicValNat p (n.choose k) = (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 b)).card
<VAR>p n k b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hnb : Nat.log p (n + k) < b<GOAL>padicValNat p ((n + k).choose k) = (Finset.filter (fun i => p ^ i ≤ k % p ^ i + n % p ^ i) (Finset.Ico 1 b)).card
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>padicValInt p ↑p = 1
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a b : ℤ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>padicValInt p (a * b) = padicValInt p a + padicValInt p b
<VAR>d : ℤ<VAR>h : 0 ≤ d<VAR>a : ℤ√d<GOAL>(Zsqrtd.toReal h) a = ↑a.re + ↑a.im * √↑d
<VAR>d : ℤ<VAR>h0d : 0 ≤ d<VAR>hd : ∀ (n : ℤ), d ≠ n * n<GOAL>Function.Injective ⇑(Zsqrtd.toReal h0d)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (𝓞 K)ˣ<VAR>w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }<GOAL>(NumberField.Units.logEmbedding K) x w = ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑x))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>∑ w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }, (NumberField.Units.logEmbedding K) x w = -↑NumberField.Units.dirichletUnitTheorem.w₀.mult * Real.log (NumberField.Units.dirichletUnitTheorem.w₀ ((algebraMap (𝓞 K) K) ↑x))
<VAR>K : Type u_1<VAR>Field K<VAR>x : (𝓞 K)ˣ<VAR>w : NumberField.InfinitePlace K<GOAL>↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0 ↔ w ((algebraMap (𝓞 K) K) ↑x) = 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>(NumberField.Units.logEmbedding K) x = 0 ↔ x ∈ NumberField.Units.torsion K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>r : ℝ<VAR>x : (𝓞 K)ˣ<VAR>hr : 0 ≤ r<VAR>h : ‖(NumberField.Units.logEmbedding K) x‖ ≤ r<VAR>w : { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }<GOAL>|(NumberField.Units.logEmbedding K) x w| ≤ r
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>r : ℝ<VAR>x : (𝓞 K)ˣ<VAR>hr : 0 ≤ r<VAR>h : ‖(NumberField.Units.logEmbedding K) x‖ ≤ r<VAR>w : NumberField.InfinitePlace K<GOAL>|Real.log (w ((algebraMap (𝓞 K) K) ↑x))| ≤ ↑(Fintype.card (NumberField.InfinitePlace K)) * r
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>r : ℝ<GOAL>(↑(NumberField.Units.unitLattice K) ∩ Metric.closedBall 0 r).Finite
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w₁ : NumberField.InfinitePlace K<VAR>B : ℕ<VAR>hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B<VAR>x : 𝓞 K<VAR>hx : x ≠ 0<GOAL>∃ y, y ≠ 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w₁ : NumberField.InfinitePlace K<VAR>B : ℕ<VAR>hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B<VAR>n : ℕ<GOAL>(algebraMap (𝓞 K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n) ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w₁ : NumberField.InfinitePlace K<VAR>B : ℕ<VAR>hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B<VAR>n : ℕ<GOAL>(Algebra.norm ℤ) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n) ≠ 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w₁ : NumberField.InfinitePlace K<VAR>B : ℕ<VAR>hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B<VAR>n m : ℕ<VAR>h : n < m<VAR>w : NumberField.InfinitePlace K<VAR>hw : w ≠ w₁<GOAL>w ((algebraMap (𝓞 K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB m)) < w ((algebraMap (𝓞 K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w₁ : NumberField.InfinitePlace K<VAR>B : ℕ<VAR>hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B<VAR>n : ℕ<GOAL>((Algebra.norm ℤ) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n)).natAbs ≤ B
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>w₁ : NumberField.InfinitePlace K<GOAL>∃ u, ∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>Submodule.span ℝ ↑(NumberField.Units.unitLattice K) = ⊤
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>FiniteDimensional.finrank ℝ ({ w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ } → ℝ) = NumberField.Units.rank K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>FiniteDimensional.finrank ℤ ↥(NumberField.Units.unitLattice K) = NumberField.Units.rank K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>(NumberField.Units.logEmbeddingQuot K) ⟦x⟧ = (NumberField.Units.logEmbedding K) x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>Function.Injective ⇑(NumberField.Units.logEmbeddingQuot K)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>↑((NumberField.Units.logEmbeddingEquiv K) ⟦x⟧) = (NumberField.Units.logEmbedding K) x
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<GOAL>FiniteDimensional.finrank ℤ (Additive ((𝓞 K)ˣ ⧸ NumberField.Units.torsion K)) = NumberField.Units.rank K
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>i : Fin (NumberField.Units.rank K)<GOAL>Additive.ofMul ⟦NumberField.Units.fundSystem K i⟧ = (NumberField.Units.basisModTorsion K) i
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x ζ : (𝓞 K)ˣ<VAR>f : Fin (NumberField.Units.rank K) → ℤ<VAR>hζ : ζ ∈ NumberField.Units.torsion K<VAR>h : x = ζ * ∏ i : Fin (NumberField.Units.rank K), NumberField.Units.fundSystem K i ^ f i<GOAL>f = ⇑((NumberField.Units.basisModTorsion K).repr (Additive.ofMul ↑x))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>∃! ζe, x = ↑ζe.1 * ∏ i : Fin (NumberField.Units.rank K), NumberField.Units.fundSystem K i ^ ζe.2 i
<VAR>z τ : ℂ<GOAL>(starRingEnd ℂ) (HurwitzZeta.jacobiTheta₂'' z τ) = HurwitzZeta.jacobiTheta₂'' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)
<VAR>z τ : ℂ<GOAL>HurwitzZeta.jacobiTheta₂'' (z + 1) τ = HurwitzZeta.jacobiTheta₂'' z τ
<VAR>z τ : ℂ<GOAL>HurwitzZeta.jacobiTheta₂'' (-z) τ = -HurwitzZeta.jacobiTheta₂'' z τ
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' z τ = -2 * ↑π / (-Complex.I * τ) ^ (3 / 2) * HurwitzZeta.jacobiTheta₂'' z (-1 / τ)
<VAR>a x : ℝ<GOAL>↑(HurwitzZeta.oddKernel (↑a) x) = HurwitzZeta.jacobiTheta₂'' (↑a) (Complex.I * ↑x)
<VAR>a x : ℝ<GOAL>↑(HurwitzZeta.oddKernel (↑a) x) = cexp (-↑π * ↑a ^ 2 * ↑x) * (jacobiTheta₂' (↑a * Complex.I * ↑x) (Complex.I * ↑x) / (2 * ↑π * Complex.I) + ↑a * jacobiTheta₂ (↑a * Complex.I * ↑x) (Complex.I * ↑x))
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>HurwitzZeta.oddKernel a x = 0
<VAR>a x : ℝ<GOAL>↑(HurwitzZeta.sinKernel (↑a) x) = jacobiTheta₂' (↑a) (Complex.I * ↑x) / (-2 * ↑π)
<VAR>a : UnitAddCircle<VAR>x : ℝ<VAR>hx : x ≤ 0<GOAL>HurwitzZeta.sinKernel a x = 0
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>HurwitzZeta.oddKernel (-a) x = -HurwitzZeta.oddKernel a x
<VAR>x : ℝ<GOAL>HurwitzZeta.oddKernel 0 x = 0
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>HurwitzZeta.sinKernel (-a) x = -HurwitzZeta.sinKernel a x
<VAR>x : ℝ<GOAL>HurwitzZeta.sinKernel 0 x = 0
<VAR>a : UnitAddCircle<GOAL>ContinuousOn (HurwitzZeta.oddKernel a) (Set.Ioi 0)
<VAR>a : UnitAddCircle<GOAL>ContinuousOn (HurwitzZeta.sinKernel a) (Set.Ioi 0)
<VAR>a : UnitAddCircle<VAR>x : ℝ<GOAL>HurwitzZeta.oddKernel a x = 1 / x ^ (3 / 2) * HurwitzZeta.sinKernel a (1 / x)
<VAR>a : ℝ<VAR>x : ℝ<VAR>hx : 0 < x<GOAL>HasSum (fun n => (↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) (HurwitzZeta.oddKernel (↑a) x)
<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => -Complex.I * ↑n * cexp (2 * ↑π * Complex.I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(HurwitzZeta.sinKernel (↑a) t)
<VAR>a : ℝ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => 2 * ↑n * Real.sin (2 * π * a * ↑n) * rexp (-π * ↑n ^ 2 * t)) (HurwitzZeta.sinKernel (↑a) t)
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ HurwitzZeta.oddKernel a =O[Filter.atTop] fun x => rexp (-p * x)
<VAR>a : UnitAddCircle<GOAL>∃ p, 0 < p ∧ HurwitzZeta.sinKernel a =O[Filter.atTop] fun x => rexp (-p * x)
<VAR>a : UnitAddCircle<GOAL>(HurwitzZeta.hurwitzOddFEPair a).k = 3 / 2
<VAR>a : UnitAddCircle<GOAL>∀ (a_1 : ℝ), (HurwitzZeta.hurwitzOddFEPair a).f a_1 = (Complex.ofReal' ∘ HurwitzZeta.oddKernel a) a_1
<VAR>a : UnitAddCircle<GOAL>(HurwitzZeta.hurwitzOddFEPair a).ε = 1
<VAR>a : UnitAddCircle<GOAL>(HurwitzZeta.hurwitzOddFEPair a).g₀ = 0
<VAR>a : UnitAddCircle<GOAL>(HurwitzZeta.hurwitzOddFEPair a).f₀ = 0
<VAR>a : UnitAddCircle<GOAL>∀ (a_1 : ℝ), (HurwitzZeta.hurwitzOddFEPair a).g a_1 = (Complex.ofReal' ∘ HurwitzZeta.sinKernel a) a_1
<VAR>a : UnitAddCircle<GOAL>Differentiable ℂ (HurwitzZeta.completedHurwitzZetaOdd a)
<VAR>a : UnitAddCircle<GOAL>Differentiable ℂ (HurwitzZeta.completedSinZeta a)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaOdd (-a) s = -HurwitzZeta.completedHurwitzZetaOdd a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedSinZeta (-a) s = -HurwitzZeta.completedSinZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedHurwitzZetaOdd a (1 - s) = HurwitzZeta.completedSinZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.completedSinZeta a (1 - s) = HurwitzZeta.completedHurwitzZetaOdd a s
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (s + 1).Gammaℝ * -Complex.I * ↑n.sign * cexp (2 * ↑π * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2) (HurwitzZeta.completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (HurwitzZeta.completedSinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (HurwitzZeta.completedHurwitzZetaOdd (↑a) s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.hurwitzZetaOdd (-a) s = -HurwitzZeta.hurwitzZetaOdd a s
<VAR>a : UnitAddCircle<GOAL>Differentiable ℂ (HurwitzZeta.hurwitzZetaOdd a)
<VAR>a : UnitAddCircle<VAR>s : ℂ<GOAL>HurwitzZeta.sinZeta (-a) s = -HurwitzZeta.sinZeta a s
<VAR>a : UnitAddCircle<GOAL>Differentiable ℂ (HurwitzZeta.sinZeta a)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (HurwitzZeta.hurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2) (HurwitzZeta.hurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>ha : a ∈ Set.Icc 0 1<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2) (HurwitzZeta.hurwitzZetaOdd (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => -Complex.I * ↑n.sign * cexp (2 * ↑π * Complex.I * ↑a * ↑n) / ↑|n| ^ s / 2) (HurwitzZeta.sinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (HurwitzZeta.sinZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesHasSum (fun x => ↑(Real.sin (2 * π * a * ↑x))) s (HurwitzZeta.sinZeta (↑a) s)
<VAR>a : UnitAddCircle<VAR>n : ℕ<GOAL>HurwitzZeta.hurwitzZetaOdd a (-2 * ↑n - 1) = 0
<VAR>a : UnitAddCircle<VAR>n : ℕ<GOAL>HurwitzZeta.sinZeta a (-2 * ↑n - 1) = 0
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<GOAL>HurwitzZeta.hurwitzZetaOdd a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * HurwitzZeta.sinZeta a s
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ -↑n<GOAL>HurwitzZeta.sinZeta a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * HurwitzZeta.hurwitzZetaOdd a s
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>self : MulChar R R'<VAR>a : R<GOAL>¬IsUnit a → (↑self.toMonoidHom).toFun a = 0
<VAR>F : Type u_3<VAR>R : outParam (Type u_4)<VAR>R' : outParam (Type u_5)<VAR>CommMonoid R<VAR>CommMonoidWithZero R'<VAR>FunLike F R R'<VAR>self : MulCharClass F R R'<VAR>χ : F<VAR>a : R<GOAL>¬IsUnit a → χ a = 0
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>x : R<GOAL>(MulChar.trivial R R') x = if IsUnit x then 1 else 0
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>f : R →* R'<VAR>hf : ∀ (a : R), ¬IsUnit a → (↑f).toFun a = 0<GOAL>⇑{ toMonoidHom := f, map_nonunit' := hf } = ⇑f
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ χ' : MulChar R R'<VAR>h : ∀ (a : R), χ a = χ' a<GOAL>χ = χ'
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>a : R<VAR>ha : ¬IsUnit a<GOAL>χ a = 0
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ χ' : MulChar R R'<VAR>h : ∀ (a : Rˣ), χ ↑a = χ' ↑a<GOAL>χ = χ'
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ χ' : MulChar R R'<GOAL>χ = χ' ↔ ∀ (a : Rˣ), χ ↑a = χ' ↑a
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>a : Rˣ<GOAL>↑(χ.toUnitHom a) = χ ↑a
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>f : Rˣ →* R'ˣ<VAR>a : Rˣ<GOAL>(MulChar.ofUnitHom f) ↑a = ↑(f a)
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ.toUnitHom = MulChar.equivToUnitHom χ
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : Rˣ →* R'ˣ<GOAL>MulChar.ofUnitHom χ = MulChar.equivToUnitHom.symm χ
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>a : Rˣ<GOAL>↑((MulChar.equivToUnitHom χ) a) = χ ↑a
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>f : Rˣ →* R'ˣ<VAR>a : Rˣ<GOAL>(MulChar.equivToUnitHom.symm f) ↑a = ↑(f a)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>CommMonoid R<VAR>χ : MulChar R R'<VAR>x : R<GOAL>χ.toMonoidHom x = χ x
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ 1 = 1
<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>R : Type u_3<VAR>CommMonoidWithZero R<VAR>Nontrivial R<VAR>χ : MulChar R R'<GOAL>χ 0 = 0
<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>R : Type u_3<VAR>CommMonoidWithZero R<VAR>Nontrivial R<VAR>χ : MulChar R R'<GOAL>∀ (a : R), ↑χ a = (↑χ.toMonoidHom).toFun a
<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>R : Type u_3<VAR>CommRing R<VAR>Nontrivial R<VAR>χ : MulChar R R'<GOAL>χ ↑(ringChar R) = 0
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>a : Rˣ<GOAL>1 ↑a = 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>x : R<VAR>hx : IsUnit x<GOAL>1 x = 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ χ' : MulChar R R'<VAR>a : R<GOAL>(χ * χ') a = χ a * χ' a
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ χ' : MulChar R R'<GOAL>⇑(χ * χ') = ⇑χ * ⇑χ'
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>1 * χ = χ
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ * 1 = χ
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>a : R<GOAL>χ⁻¹ a = Ring.inverse (χ a)
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_3<VAR>Field R'<VAR>χ : MulChar R R'<VAR>a : R<GOAL>χ⁻¹ a = (χ a)⁻¹
<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>R : Type u_3<VAR>CommMonoidWithZero R<VAR>χ : MulChar R R'<VAR>a : R<GOAL>χ⁻¹ a = χ (Ring.inverse a)
<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>R : Type u_3<VAR>Field R<VAR>χ : MulChar R R'<VAR>a : R<GOAL>χ⁻¹ a = χ a⁻¹
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ⁻¹ * χ = 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>n : ℕ<VAR>a : Rˣ<GOAL>(χ ^ n) ↑a = χ ↑a ^ n
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : R<GOAL>(χ ^ n) a = χ a ^ n
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ₁ χ₂ : MulChar R R'<VAR>a : Rˣ<GOAL>(MulChar.equivToUnitHom (χ₁ * χ₂)) a = (MulChar.equivToUnitHom χ₁) a * (MulChar.equivToUnitHom χ₂) a
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ = 1 ↔ ∀ (a : Rˣ), χ ↑a = 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ ≠ 1 ↔ ∃ a, χ ↑a ≠ 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<GOAL>χ.IsNontrivial ↔ χ ≠ 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>χ : MulChar R ℤ<VAR>hχ : χ.IsQuadratic<VAR>χ' : MulChar R' ℤ<VAR>hχ' : χ'.IsQuadratic<VAR>Nontrivial R''<VAR>hR'' : ringChar R'' ≠ 2<VAR>a : R<VAR>a' : R'<VAR>h : ↑(χ a) = ↑(χ' a')<GOAL>χ a = χ' a'
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>χ : MulChar R R'<VAR>f : R' →+* R''<VAR>a : R<GOAL>(χ.ringHomComp f) a = f (χ a)
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>f : R' →+* R''<GOAL>MulChar.ringHomComp 1 f = 1
<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>R : Type u_4<VAR>CommRing R<VAR>χ : MulChar R R'<VAR>f : R' →+* R''<GOAL>(χ.ringHomComp f)⁻¹ = χ⁻¹.ringHomComp f
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>χ φ : MulChar R R'<VAR>f : R' →+* R''<GOAL>(χ * φ).ringHomComp f = χ.ringHomComp f * φ.ringHomComp f
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>χ : MulChar R R'<VAR>f : R' →+* R''<VAR>n : ℕ<GOAL>χ.ringHomComp f ^ n = (χ ^ n).ringHomComp f
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>f : R' →+* R''<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective fun x => x.ringHomComp f
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>f : R' →+* R''<VAR>hf : Function.Injective ⇑f<VAR>χ : MulChar R R'<GOAL>χ.ringHomComp f = 1 ↔ χ = 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>f : R' →+* R''<VAR>hf : Function.Injective ⇑f<VAR>χ : MulChar R R'<GOAL>χ.ringHomComp f ≠ 1 ↔ χ ≠ 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>χ : MulChar R R'<VAR>hχ : χ.IsNontrivial<VAR>f : R' →+* R''<VAR>hf : Function.Injective ⇑f<GOAL>(χ.ringHomComp f).IsNontrivial
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>R'' : Type u_3<VAR>CommRing R''<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>f : R' →+* R''<GOAL>(χ.ringHomComp f).IsQuadratic
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<GOAL>χ⁻¹ = χ
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<GOAL>χ ^ 2 = 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>CharP R' p<GOAL>χ ^ p = χ
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>n : ℕ<VAR>hn : Even n<GOAL>χ ^ n = 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsQuadratic<VAR>n : ℕ<VAR>hn : Odd n<GOAL>χ ^ n = χ
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>Fintype Mˣ<VAR>χ : MulChar M R<GOAL>χ ^ Fintype.card Mˣ = 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>R : Type u_2<VAR>CommMonoidWithZero R<VAR>Finite Mˣ<VAR>χ : MulChar M R<GOAL>0 < orderOf χ
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>Fintype R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ ≠ 1<GOAL>∑ a : R, χ a = 0
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>Fintype R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>IsDomain R'<VAR>χ : MulChar R R'<VAR>hχ : χ.IsNontrivial<GOAL>∑ a : R, χ a = 0
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>Fintype R<VAR>R' : Type u_2<VAR>CommRing R'<VAR>DecidableEq R<GOAL>∑ a : R, 1 a = ↑(Fintype.card Rˣ)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>CommRing R<VAR>CommMonoidWithZero R'<VAR>χ : MulChar R R'<VAR>n : ℕ<VAR>hn : Odd n<VAR>hχ : χ ^ n = 1<GOAL>χ (-1) = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x y : ℤ_[p]<GOAL>↑x = ↑y → x = y
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x : ℚ_[p]<GOAL>x ∈ PadicInt.subring p ↔ ‖x‖ ≤ 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>h : ‖0‖ ≤ 1<GOAL>⟨0, h⟩ = 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<GOAL>↑(z1 + z2) = ↑z1 + ↑z2
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<GOAL>↑(z1 * z2) = ↑z1 * ↑z2
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z1 : ℤ_[p]<GOAL>↑(-z1) = -↑z1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<GOAL>↑(z1 - z2) = ↑z1 - ↑z2
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>↑1 = 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<GOAL>↑0 = 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>↑z = 0 ↔ z = 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>↑z ≠ 0 ↔ z ≠ 0
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>n : ℕ<GOAL>↑↑n = ↑n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z : ℤ<GOAL>↑↑z = ↑z
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>x : ℤ_[p]<VAR>n : ℕ<GOAL>↑(x ^ n) = ↑x ^ n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>k : ℤ_[p]<GOAL>⟨↑k, ⋯⟩ = k
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z1 z2 : ℤ<GOAL>↑z1 = ↑z2 ↔ z1 = z2
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>‖z‖ = ‖↑z‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>‖z‖ ≤ 1
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<GOAL>‖z1 * z2‖ = ‖z1‖ * ‖z2‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z : ℤ_[p]<VAR>n : ℕ<GOAL>‖z ^ n‖ = ‖z‖ ^ n
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q r : ℤ_[p]<GOAL>‖q + r‖ ≤ max ‖q‖ ‖r‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>q r : ℤ_[p]<GOAL>‖q‖ ≠ ‖r‖ → ‖q + r‖ = max ‖q‖ ‖r‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<VAR>h : ‖z1 + z2‖ < ‖z2‖<GOAL>‖z1‖ = ‖z2‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z1 z2 : ℤ_[p]<VAR>h : ‖z1 + z2‖ < ‖z1‖<GOAL>‖z1‖ = ‖z2‖
<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>z : ℤ_[p]<GOAL>‖↑z‖ = ‖z‖