ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>φ.order.Dom ↔ φ ≠ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>h : φ.order.Dom<GOAL>(PowerSeries.coeff R (φ.order.get h)) φ ≠ 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>n : ℕ<VAR>h : (PowerSeries.coeff R n) φ ≠ 0<GOAL>φ.order ≤ ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>n : ℕ<VAR>h : ↑n < φ.order<GOAL>(PowerSeries.coeff R n) φ = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>φ.order = ⊤ ↔ φ = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>n : ℕ<VAR>h : ∀ i < n, (PowerSeries.coeff R i) φ = 0<GOAL>↑n ≤ φ.order
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>n : PartENat<VAR>h : ∀ (i : ℕ), ↑i < n → (PowerSeries.coeff R i) φ = 0<GOAL>n ≤ φ.order
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>n : ℕ<GOAL>φ.order = ↑n ↔ (PowerSeries.coeff R n) φ ≠ 0 ∧ ∀ i < n, (PowerSeries.coeff R i) φ = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>n : PartENat<GOAL>φ.order = n ↔ (∀ (i : ℕ), ↑i = n → (PowerSeries.coeff R i) φ ≠ 0) ∧ ∀ (i : ℕ), ↑i < n → (PowerSeries.coeff R i) φ = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ ψ : PowerSeries R<GOAL>min φ.order ψ.order ≤ (φ + ψ).order
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ ψ : PowerSeries R<VAR>_h : φ.order ≠ ψ.order<VAR>H : φ.order < ψ.order<GOAL>(φ + ψ).order ≤ φ.order ⊓ ψ.order
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ ψ : PowerSeries R<VAR>h : φ.order ≠ ψ.order<GOAL>(φ + ψ).order = φ.order ⊓ ψ.order
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ ψ : PowerSeries R<GOAL>φ.order + ψ.order ≤ (φ * ψ).order
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<VAR>Decidable (a = 0)<GOAL>((PowerSeries.monomial R n) a).order = if a = 0 then ⊤ else ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<VAR>h : a ≠ 0<GOAL>((PowerSeries.monomial R n) a).order = ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ ψ : PowerSeries R<VAR>n : ℕ<VAR>h : ↑n < ψ.order<GOAL>(PowerSeries.coeff R n) (φ * ψ) = 0
<VAR>R : Type u_2<VAR>CommRing R<VAR>φ ψ : PowerSeries R<VAR>n : ℕ<VAR>h : ↑n < ψ.order<GOAL>(PowerSeries.coeff R n) (φ * (1 - ψ)) = (PowerSeries.coeff R n) φ
<VAR>R : Type u_2<VAR>ι : Type u_3<VAR>CommRing R<VAR>k : ℕ<VAR>s : Finset ι<VAR>φ : PowerSeries R<VAR>f : ι → PowerSeries R<GOAL>(∀ i ∈ s, ↑k < (f i).order) → (PowerSeries.coeff R k) (φ * ∏ i ∈ s, (1 - f i)) = (PowerSeries.coeff R k) φ
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<VAR>h : φ.order.Dom<GOAL>PowerSeries.X ^ φ.order.get h ∣ φ
<VAR>R : Type u_2<VAR>Semiring R<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>φ : PowerSeries R<GOAL>φ.order = multiplicity PowerSeries.X φ
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : PowerSeries R<VAR>hf : f ≠ 0<GOAL>PowerSeries.X ^ f.order.get ⋯ * PowerSeries.divided_by_X_pow_order hf = f
<VAR>R : Type u_1<VAR>Semiring R<VAR>Nontrivial R<GOAL>PowerSeries.order 1 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>Nontrivial R<VAR>f : PowerSeries R<GOAL>IsUnit f → f.order = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>Nontrivial R<GOAL>PowerSeries.X.order = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>Nontrivial R<VAR>n : ℕ<GOAL>(PowerSeries.X ^ n).order = ↑n
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>φ ψ : PowerSeries R<GOAL>(φ * ψ).order = φ.order + ψ.order
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>PowerSeries.divided_by_X_pow_order ⋯ = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>f g : PowerSeries R<VAR>hf : f ≠ 0<VAR>hg : g ≠ 0<GOAL>PowerSeries.divided_by_X_pow_order hf * PowerSeries.divided_by_X_pow_order hg = PowerSeries.divided_by_X_pow_order ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : Kˣ<GOAL>↑(v.valuationOfNeZeroToFun x) = v.valuation ↑x
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : Kˣ<GOAL>↑(v.valuationOfNeZero x) = v.valuation ↑x
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : Rˣ<GOAL>v.valuationOfNeZero ((Units.map ↑(algebraMap R K)) x) = 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>n : ℕ<VAR>x : Rˣ<GOAL>(v.valuationOfNeZeroMod n) ↑((Units.map ↑(algebraMap R K)) x) = 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>S S' : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>n : ℕ<VAR>hS : S ≤ S'<GOAL>IsDedekindDomain.selmerGroup ≤ IsDedekindDomain.selmerGroup
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>n : ℕ<GOAL>IsDedekindDomain.selmerGroup.valuation.ker = IsDedekindDomain.selmerGroup.subgroupOf IsDedekindDomain.selmerGroup
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>n : ℕ<VAR>hn : Fact (0 < n)<GOAL>IsDedekindDomain.selmerGroup.fromUnit.ker = (powMonoidHom n).range
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>n : ℕ<VAR>Fact (0 < n)<GOAL>Function.Injective ⇑IsDedekindDomain.selmerGroup.fromUnitLift
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>D1 D2 : Derivation R A A<GOAL>↑⁅D1, D2⁆ = ⁅↑D1, ↑D2⁆
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>D1 D2 : Derivation R A A<VAR>a : A<GOAL>⁅D1, D2⁆ a = D1 (D2 a) - D2 (D1 a)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : DedekindDomain.FiniteIntegralAdeles R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>(fun v => ↑(x v)) v = ↑(x v)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : DedekindDomain.FiniteIntegralAdeles R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>(DedekindDomain.FiniteIntegralAdeles.Coe.addMonoidHom R K) x v = ↑(x v)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : DedekindDomain.FiniteIntegralAdeles R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>(DedekindDomain.FiniteIntegralAdeles.Coe.ringHom R K) x v = ↑(x v)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>k : K<GOAL>(algebraMap K (DedekindDomain.ProdAdicCompletions R K)) k v = ↑K k
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>(algebraMap R (DedekindDomain.ProdAdicCompletions R K)) r v = ↑K ((algebraMap R K) r)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : DedekindDomain.FiniteIntegralAdeles R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>(DedekindDomain.FiniteIntegralAdeles.Coe.algHom R K) x v = ↑(x v)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : DedekindDomain.ProdAdicCompletions R K<GOAL>x.IsFiniteAdele ↔ {v | x v ∉ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x y : DedekindDomain.ProdAdicCompletions R K<VAR>hx : x.IsFiniteAdele<VAR>hy : y.IsFiniteAdele<GOAL>(x + y).IsFiniteAdele
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>DedekindDomain.ProdAdicCompletions.IsFiniteAdele 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : DedekindDomain.ProdAdicCompletions R K<VAR>hx : x.IsFiniteAdele<GOAL>(-x).IsFiniteAdele
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x y : DedekindDomain.ProdAdicCompletions R K<VAR>hx : x.IsFiniteAdele<VAR>hy : y.IsFiniteAdele<GOAL>(x * y).IsFiniteAdele
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>DedekindDomain.ProdAdicCompletions.IsFiniteAdele 1
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>k : K<GOAL>((algebraMap K (DedekindDomain.ProdAdicCompletions R K)) k).IsFiniteAdele
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>a₁ a₂ : DedekindDomain.FiniteAdeleRing R K<VAR>h : ↑a₁ = ↑a₂<GOAL>a₁ = a₂
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>a : DedekindDomain.FiniteAdeleRing R K<GOAL>(∃ c, a = ↑c) ↔ ∀ (v : IsDedekindDomain.HeightOneSpectrum R), (fun v => ↑a v) v ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>a : DedekindDomain.FiniteAdeleRing R K<GOAL>∃ b c, a * ↑↑b = ↑c
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>SubmodulesRingBasis fun r => Submodule.span (DedekindDomain.FiniteIntegralAdeles R K) {↑↑r}
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ+<VAR>ζ : Mˣ<GOAL>ζ ∈ rootsOfUnity k M ↔ ζ ^ ↑k = 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ+<VAR>ζ : Mˣ<GOAL>ζ ∈ rootsOfUnity k M ↔ ↑ζ ^ ↑k = 1
<VAR>M : Type u_7<VAR>CommMonoid M<GOAL>rootsOfUnity 1 M = ⊥
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>n : ℕ+<GOAL>Function.Injective fun x => ↑↑x
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : M<VAR>n : ℕ+<VAR>h : ζ ^ ↑n = 1<GOAL>↑↑(rootsOfUnity.mkOfPowEq ζ h) = ζ
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k l : ℕ+<VAR>h : k ∣ l<GOAL>rootsOfUnity k M ≤ rootsOfUnity l M
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>CommMonoid M<VAR>CommMonoid N<VAR>f : Mˣ →* Nˣ<VAR>k : ℕ+<GOAL>Subgroup.map f (rootsOfUnity k M) ≤ rootsOfUnity k N
<VAR>R : Type u_4<VAR>k : ℕ+<VAR>CommMonoid R<VAR>ζ : ↥(rootsOfUnity k R)<VAR>m : ℕ<GOAL>↑↑(ζ ^ m) = ↑↑ζ ^ m
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>F : Type u_6<VAR>k : ℕ+<VAR>CommMonoid R<VAR>CommMonoid S<VAR>FunLike F R S<VAR>MonoidHomClass F R S<VAR>σ : F<VAR>ζ : ↥(rootsOfUnity k R)<GOAL>↑↑((restrictRootsOfUnity σ k) ζ) = σ ↑↑ζ
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>k : ℕ+<VAR>CommMonoid R<VAR>CommMonoid S<VAR>σ : R ≃* S<VAR>ζ : ↥(rootsOfUnity k R)<GOAL>↑↑((σ.restrictRootsOfUnity k) ζ) = σ ↑↑ζ
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>k : ℕ+<VAR>CommMonoid R<VAR>CommMonoid S<VAR>σ : R ≃* S<GOAL>(σ.restrictRootsOfUnity k).symm = σ.symm.restrictRootsOfUnity k
<VAR>R : Type u_4<VAR>k : ℕ+<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : Rˣ<GOAL>ζ ∈ rootsOfUnity k R ↔ ↑ζ ∈ Polynomial.nthRoots (↑k) 1
<VAR>R : Type u_4<VAR>k : ℕ+<VAR>CommRing R<VAR>IsDomain R<VAR>x : ↥(rootsOfUnity k R)<GOAL>↑((rootsOfUnityEquivNthRoots R k) x) = ↑↑x
<VAR>R : Type u_4<VAR>k : ℕ+<VAR>CommRing R<VAR>IsDomain R<VAR>x : { x // x ∈ Polynomial.nthRoots (↑k) 1 }<GOAL>↑↑((rootsOfUnityEquivNthRoots R k).symm x) = ↑x
<VAR>R : Type u_4<VAR>k : ℕ+<VAR>CommRing R<VAR>IsDomain R<GOAL>Fintype.card ↥(rootsOfUnity k R) ≤ ↑k
<VAR>R : Type u_4<VAR>F : Type u_6<VAR>k : ℕ+<VAR>CommRing R<VAR>IsDomain R<VAR>FunLike F R R<VAR>RingHomClass F R R<VAR>σ : F<VAR>ζ : ↥(rootsOfUnity k R)<GOAL>∃ m, σ ↑↑ζ = ↑↑ζ ^ m
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsReduced R<VAR>p k : ℕ<VAR>m : ℕ+<VAR>ExpChar R p<VAR>ζ : Rˣ<GOAL>ζ ∈ rootsOfUnity (⟨p, ⋯⟩ ^ k * m) R ↔ ζ ∈ rootsOfUnity m R
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsReduced R<VAR>p k : ℕ<VAR>m : ℕ+<VAR>ExpChar R p<VAR>ζ : Rˣ<GOAL>ζ ^ (p ^ k * ↑m) = 1 ↔ ζ ∈ rootsOfUnity m R
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : M<VAR>k : ℕ<GOAL>IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : M<VAR>k : ℕ<VAR>self : IsPrimitiveRoot ζ k<VAR>l : ℕ<GOAL>ζ ^ l = 1 → k ∣ l
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : M<VAR>k : ℕ<VAR>self : IsPrimitiveRoot ζ k<GOAL>ζ ^ k = 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>μ : M<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot μ ↑n<GOAL>↑(↑h.toRootsOfUnity)⁻¹ = μ ^ (↑n - 1)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>μ : M<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot μ ↑n<GOAL>↑↑h.toRootsOfUnity = μ
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>h0 : 0 < k<GOAL>ζ ∈ primitiveRoots k R ↔ IsPrimitiveRoot ζ k
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<GOAL>primitiveRoots 0 R = ∅
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>h : ζ ∈ primitiveRoots k R<GOAL>IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>hk : 0 < k<VAR>h1 : ζ ^ k = 1<VAR>h : ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1<GOAL>IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>Subsingleton M<VAR>x : M<GOAL>IsPrimitiveRoot x 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℕ<GOAL>ζ ^ l = 1 ↔ k ∣ l
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>h0 : 0 < k<GOAL>IsUnit ζ
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k l : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>h0 : 0 < l<VAR>hl : l < k<GOAL>ζ ^ l ≠ 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>hk : 1 < k<GOAL>ζ ≠ 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>i j : ℕ<VAR>hi : i < k<VAR>hj : j < k<VAR>H : ζ ^ i = ζ ^ j<GOAL>i = j
<VAR>M : Type u_1<VAR>CommMonoid M<GOAL>IsPrimitiveRoot 1 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : M<GOAL>IsPrimitiveRoot ζ 1 ↔ ζ = 1
<VAR>k : ℕ<VAR>M : Type u_7<VAR>B : Type u_8<VAR>CommMonoid M<VAR>SetLike B M<VAR>SubmonoidClass B M<VAR>N : B<VAR>ζ : ↥N<GOAL>IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : Mˣ<GOAL>IsPrimitiveRoot (↑ζ) k ↔ IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : M<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>IsPrimitiveRoot ⋯.unit n
<VAR>G : Type u_3<VAR>DivisionCommMonoid G<VAR>ζ : G<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>IsPrimitiveRoot ⋯.unit' n
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℕ<VAR>hi : i.Coprime k<GOAL>IsPrimitiveRoot (ζ ^ i) k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>p : ℕ<VAR>hprime : Nat.Prime p<VAR>hdiv : ¬p ∣ k<GOAL>IsPrimitiveRoot (ζ ^ p) k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>h0 : 0 < k<VAR>i : ℕ<GOAL>IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : M<GOAL>IsPrimitiveRoot ζ (orderOf ζ)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k l : ℕ<VAR>ζ : M<VAR>hk : IsPrimitiveRoot ζ k<VAR>hl : IsPrimitiveRoot ζ l<GOAL>k = l
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<GOAL>k = orderOf ζ
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>hk : 0 < k<GOAL>IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), 0 < l → l < k → ζ ^ l ≠ 1
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<GOAL>¬IsPrimitiveRoot ζ k ↔ orderOf ζ ≠ k
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ ζ' : M<VAR>k' : ℕ<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hζ' : IsPrimitiveRoot ζ' k'<VAR>hk : k ≠ 0<VAR>hk' : k' ≠ 0<GOAL>IsPrimitiveRoot (ζ ^ (k / k.factorizationLCMLeft k') * ζ' ^ (k' / k.factorizationLCMRight k')) (k.lcm k')
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>k : ℕ<VAR>ζ : M<VAR>h : IsPrimitiveRoot ζ k<VAR>p : ℕ<VAR>hp : p ≠ 0<VAR>hdiv : p ∣ k<GOAL>IsPrimitiveRoot (ζ ^ p) (k / p)
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : Mˣ<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<GOAL>ζ ∈ rootsOfUnity n M
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>ζ : M<VAR>n a b : ℕ<VAR>hn : 0 < n<VAR>h : IsPrimitiveRoot ζ n<VAR>hprod : n = a * b<GOAL>IsPrimitiveRoot (ζ ^ a) b
<VAR>M : Type u_1<VAR>CommMonoid M<VAR>n : ℕ<VAR>ζ : M<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>Set.InjOn (fun x => ζ ^ x) ↑(Finset.range n)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>F : Type u_6<VAR>CommMonoid M<VAR>CommMonoid N<VAR>k : ℕ<VAR>ζ : M<VAR>f : F<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>h : IsPrimitiveRoot ζ k<VAR>hf : Function.Injective ⇑f<GOAL>IsPrimitiveRoot (f ζ) k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>F : Type u_6<VAR>CommMonoid M<VAR>CommMonoid N<VAR>k : ℕ<VAR>ζ : M<VAR>f : F<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>h : IsPrimitiveRoot (f ζ) k<VAR>hf : Function.Injective ⇑f<GOAL>IsPrimitiveRoot ζ k
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>F : Type u_6<VAR>CommMonoid M<VAR>CommMonoid N<VAR>k : ℕ<VAR>ζ : M<VAR>f : F<VAR>FunLike F M N<VAR>MonoidHomClass F M N<VAR>hf : Function.Injective ⇑f<GOAL>IsPrimitiveRoot (f ζ) k ↔ IsPrimitiveRoot ζ k
<VAR>M₀ : Type u_7<VAR>CommMonoidWithZero M₀<VAR>Nontrivial M₀<GOAL>IsPrimitiveRoot 0 0
<VAR>k : ℕ<VAR>M₀ : Type u_7<VAR>CommMonoidWithZero M₀<VAR>Nontrivial M₀<VAR>ζ : M₀<VAR>h : IsPrimitiveRoot ζ k<GOAL>k ≠ 0 → ζ ≠ 0
<VAR>M₀ : Type u_7<VAR>CancelCommMonoidWithZero M₀<VAR>n : ℕ<VAR>ζ : M₀<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α : M₀<VAR>hα : α ≠ 0<GOAL>Set.InjOn (fun x => ζ ^ x * α) ↑(Finset.range n)
<VAR>G : Type u_3<VAR>DivisionCommMonoid G<VAR>k : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<GOAL>ζ ^ ↑k = 1
<VAR>G : Type u_3<VAR>DivisionCommMonoid G<VAR>k : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>l : ℤ<GOAL>ζ ^ l = 1 ↔ ↑k ∣ l
<VAR>G : Type u_3<VAR>DivisionCommMonoid G<VAR>k : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<GOAL>IsPrimitiveRoot ζ⁻¹ k
<VAR>G : Type u_3<VAR>DivisionCommMonoid G<VAR>k : ℕ<VAR>ζ : G<GOAL>IsPrimitiveRoot ζ⁻¹ k ↔ IsPrimitiveRoot ζ k
<VAR>G : Type u_3<VAR>DivisionCommMonoid G<VAR>k : ℕ<VAR>ζ : G<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<VAR>hi : i.gcd ↑k = 1<GOAL>IsPrimitiveRoot (ζ ^ i) k
<VAR>R : Type u_4<VAR>CommRing R<VAR>n : ℕ<VAR>hn : 1 < n<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<GOAL>ζ - 1 ≠ 0
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<GOAL>primitiveRoots 1 R = {1}
<VAR>R : Type u_4<VAR>ζ : R<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<GOAL>NeZero ↑↑n
<VAR>R : Type u_4<VAR>k : ℕ<VAR>ζ : R<VAR>CommRing R<VAR>IsDomain R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hk : 0 < k<GOAL>ζ ∈ Polynomial.nthRootsFinset k R
<VAR>R : Type u_4<VAR>CommRing R<VAR>NoZeroDivisors R<VAR>ζ : R<VAR>h : IsPrimitiveRoot ζ 2<GOAL>ζ = -1
<VAR>R : Type u_4<VAR>CommRing R<VAR>p : ℕ<VAR>Nontrivial R<VAR>h : CharP R p<VAR>hp : p ≠ 2<GOAL>IsPrimitiveRoot (-1) 2
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hk : 1 < k<GOAL>∑ i ∈ Finset.range k, ζ ^ i = 0
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>hk : 1 < k<GOAL>ζ ^ k.pred = -∑ i ∈ Finset.range k.pred, ζ ^ i
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<GOAL>h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℕ<GOAL>h.zmodEquivZPowers ↑i = Additive.ofMul ⟨ζ ^ i, ⋯⟩
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<GOAL>h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℤ<GOAL>h.zmodEquivZPowers.symm ⟨ζ ^ i, ⋯⟩ = ↑i
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℕ<GOAL>h.zmodEquivZPowers.symm (Additive.ofMul ⟨ζ ^ i, ⋯⟩) = ↑i
<VAR>R : Type u_4<VAR>k : ℕ<VAR>CommRing R<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ k<VAR>i : ℕ<GOAL>h.zmodEquivZPowers.symm ⟨ζ ^ i, ⋯⟩ = ↑i
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>k : ℕ+<VAR>ζ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<GOAL>Subgroup.zpowers ζ = rootsOfUnity k R
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>S : Type u_7<VAR>F : Type u_8<VAR>CommRing S<VAR>IsDomain S<VAR>FunLike F R S<VAR>MonoidHomClass F R S<VAR>ζ : R<VAR>n : ℕ+<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>Subgroup.map (Units.map ↑f) (rootsOfUnity n R) = rootsOfUnity n S
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>S : Type u_7<VAR>F : Type u_8<VAR>CommRing S<VAR>IsDomain S<VAR>FunLike F R S<VAR>MonoidHomClass F R S<VAR>n : ℕ+<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>hζ : (primitiveRoots (↑n) R).Nonempty<GOAL>∀ (a : ↥(rootsOfUnity n R)), ⋯ = ⋯
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>S : Type u_7<VAR>F : Type u_8<VAR>CommRing S<VAR>IsDomain S<VAR>FunLike F R S<VAR>MonoidHomClass F R S<VAR>n : ℕ+<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>hζ : (primitiveRoots (↑n) R).Nonempty<GOAL>∀ (a : ↥(rootsOfUnity n R)), ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ) a) = f ↑↑a
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>S : Type u_7<VAR>F : Type u_8<VAR>CommRing S<VAR>IsDomain S<VAR>FunLike F R S<VAR>MonoidHomClass F R S<VAR>n : ℕ+<VAR>f : F<VAR>hf : Function.Injective ⇑f<VAR>hζ : (primitiveRoots (↑n) R).Nonempty<VAR>η : ↥(rootsOfUnity n S)<GOAL>f ↑↑((rootsOfUnityEquivOfPrimitiveRoots hf hζ).symm η) = ↑↑η
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>k : ℕ+<VAR>ζ ξ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<VAR>hξ : ξ ∈ rootsOfUnity k R<GOAL>∃ i < ↑k, ζ ^ i = ξ
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>k : ℕ<VAR>hk : 0 < k<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ k<VAR>ξ : Rˣ<VAR>hξ : ξ ∈ rootsOfUnity ⟨k, hk⟩ R<GOAL>∃ i < k, ζ ^ i = ↑ξ
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>k : ℕ<VAR>ζ ξ : R<VAR>h : IsPrimitiveRoot ζ k<VAR>hξ : ξ ^ k = 1<VAR>h0 : 0 < k<GOAL>∃ i < k, ζ ^ i = ξ
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>k : ℕ+<VAR>ζ ξ : Rˣ<VAR>h : IsPrimitiveRoot ζ ↑k<GOAL>IsPrimitiveRoot ξ ↑k ↔ ∃ i < ↑k, i.Coprime ↑k ∧ ζ ^ i = ξ
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>k : ℕ<VAR>ζ ξ : R<VAR>h : IsPrimitiveRoot ζ k<VAR>h0 : 0 < k<GOAL>IsPrimitiveRoot ξ k ↔ ∃ i < k, i.Coprime k ∧ ζ ^ i = ξ
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<VAR>α a : R<VAR>e : α ^ n = a<GOAL>Polynomial.nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>n : ℕ<VAR>ζ : R<VAR>hζ : IsPrimitiveRoot ζ n<VAR>a : R<GOAL>Multiset.card (Polynomial.nthRoots n a) = if ∃ α, α ^ n = a then n else 0
<VAR>R : Type u_4<VAR>CommRing R<VAR>ζ : Rˣ<VAR>IsDomain R<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<GOAL>Fintype.card ↥(rootsOfUnity n R) = ↑n
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<GOAL>Fintype.card ↥(rootsOfUnity n R) = ↑n
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>Multiset.card (Polynomial.nthRoots n 1) = n
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<VAR>a : R<VAR>ha : a ≠ 0<GOAL>(Polynomial.nthRoots n a).Nodup
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>(Polynomial.nthRoots n 1).Nodup
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<GOAL>(Polynomial.nthRootsFinset n R).card = n
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>k : ℕ<VAR>h : IsPrimitiveRoot ζ k<GOAL>(primitiveRoots k R).card = k.totient
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>k l : ℕ<VAR>h : k ≠ l<GOAL>Disjoint (primitiveRoots k R) (primitiveRoots l R)
<VAR>R : Type u_4<VAR>CommRing R<VAR>IsDomain R<VAR>ζ : R<VAR>n : ℕ+<VAR>h : IsPrimitiveRoot ζ ↑n<GOAL>Polynomial.nthRootsFinset (↑n) R = (↑n).divisors.biUnion fun i => primitiveRoots i R