ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>φ : ι → MvPolynomial σ R<VAR>n : M<VAR>w : σ → M<VAR>h : ∀ i ∈ s, MvPolynomial.IsWeightedHomogeneous w (φ i) n<GOAL>MvPolynomial.IsWeightedHomogeneous w (∑ i ∈ s, φ i) n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>φ ψ : MvPolynomial σ R<VAR>m n : M<VAR>w : σ → M<VAR>hφ : MvPolynomial.IsWeightedHomogeneous w φ m<VAR>hψ : MvPolynomial.IsWeightedHomogeneous w ψ n<GOAL>MvPolynomial.IsWeightedHomogeneous w (φ * ψ) (m + n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>φ : ι → MvPolynomial σ R<VAR>n : ι → M<VAR>w : σ → M<GOAL>(∀ i ∈ s, MvPolynomial.IsWeightedHomogeneous w (φ i) (n i)) → MvPolynomial.IsWeightedHomogeneous w (∏ i ∈ s, φ i) (∑ i ∈ s, n i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>φ : MvPolynomial σ R<VAR>n : M<VAR>SemilatticeSup M<VAR>w : σ → M<VAR>hφ : MvPolynomial.IsWeightedHomogeneous w φ n<VAR>h : φ ≠ 0<GOAL>MvPolynomial.weightedTotalDegree' w φ = ↑n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<GOAL>SetLike.GradedMonoid (MvPolynomial.weightedHomogeneousSubmodule R w)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ : MvPolynomial σ R<VAR>DecidableEq M<VAR>d : σ →₀ ℕ<GOAL>MvPolynomial.coeff d ((MvPolynomial.weightedHomogeneousComponent w n) φ) = if (Finsupp.weight w) d = n then MvPolynomial.coeff d φ else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ : MvPolynomial σ R<VAR>DecidableEq M<GOAL>(MvPolynomial.weightedHomogeneousComponent w n) φ = ∑ d ∈ Finset.filter (fun d => (Finsupp.weight w) d = n) φ.support, (MvPolynomial.monomial d) (MvPolynomial.coeff d φ)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.weightedHomogeneousComponent w n) φ) n
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>m : M<GOAL>(MvPolynomial.weightedHomogeneousComponent w m) φ ∈ MvPolynomial.weightedHomogeneousSubmodule R w m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>n : M<VAR>r : R<GOAL>(MvPolynomial.weightedHomogeneousComponent w n) (MvPolynomial.C r * φ) = MvPolynomial.C r * (MvPolynomial.weightedHomogeneousComponent w n) φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ : MvPolynomial σ R<VAR>h : ∀ d ∈ φ.support, (Finsupp.weight w) d ≠ n<GOAL>(MvPolynomial.weightedHomogeneousComponent w n) φ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>n : M<VAR>φ : MvPolynomial σ R<VAR>SemilatticeSup M<VAR>OrderBot M<VAR>h : MvPolynomial.weightedTotalDegree w φ < n<GOAL>(MvPolynomial.weightedHomogeneousComponent w n) φ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<GOAL>(Function.support fun m => (MvPolynomial.weightedHomogeneousComponent w m) φ).Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<GOAL>∑ᶠ (m : M), (MvPolynomial.weightedHomogeneousComponent w m) φ = φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>m : M<VAR>p : MvPolynomial σ R<VAR>hp : MvPolynomial.IsWeightedHomogeneous w p m<GOAL>(MvPolynomial.weightedHomogeneousComponent w m) p = p
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>m : M<VAR>n : M<VAR>p : MvPolynomial σ R<VAR>hp : MvPolynomial.IsWeightedHomogeneous w p m<GOAL>n ≠ m → (MvPolynomial.weightedHomogeneousComponent w n) p = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>DecidableEq M<VAR>m n : M<VAR>p : MvPolynomial σ R<VAR>h : p ∈ MvPolynomial.weightedHomogeneousSubmodule R w n<GOAL>(MvPolynomial.weightedHomogeneousComponent w m) p = if m = n then p else 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>m n : M<VAR>p : MvPolynomial σ R<VAR>hp : MvPolynomial.IsWeightedHomogeneous w p m<VAR>hn : n ≠ m<GOAL>(MvPolynomial.weightedHomogeneousComponent w n) p = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>DecidableEq σ<VAR>DecidableEq R<VAR>DecidableEq M<VAR>x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)<GOAL>(DirectSum.coeLinearMap fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun x x_1 => ↑x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>DecidableEq σ<VAR>DecidableEq R<VAR>DecidableEq M<VAR>x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)<GOAL>(DirectSum.coeAddMonoidHom fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x = DFinsupp.sum x fun x x_1 => ↑x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>DecidableEq M<VAR>x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)<GOAL>(DirectSum.coeLinearMap fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x = ∑ᶠ (m : M), ↑(x m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>AddCommMonoid M<VAR>w : σ → M<VAR>DecidableEq M<VAR>x : DirectSum M fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)<VAR>m : M<GOAL>(MvPolynomial.weightedHomogeneousComponent w m) ((DirectSum.coeLinearMap fun i => MvPolynomial.weightedHomogeneousSubmodule R w i) x) = ↑(x m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>CanonicallyOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>NoZeroSMulDivisors ℕ M<VAR>hw : ∀ (i : σ), w i ≠ 0<GOAL>(MvPolynomial.weightedHomogeneousComponent w 0) φ = MvPolynomial.C (MvPolynomial.coeff 0 φ)
<VAR>M : Type u_2<VAR>σ : Type u_3<VAR>CanonicallyOrderedAddCommMonoid M<VAR>w : σ → M<VAR>NoZeroSMulDivisors ℕ M<VAR>hw : ∀ (i : σ), w i ≠ 0<GOAL>MvPolynomial.NonTorsionWeight w
<VAR>M : Type u_2<VAR>σ : Type u_3<VAR>CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>hw : MvPolynomial.NonTorsionWeight w<VAR>m : σ →₀ ℕ<GOAL>(Finsupp.weight w) m = 0 ↔ ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.IsWeightedHomogeneous w p 0 ↔ MvPolynomial.weightedTotalDegree w p = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>hw : MvPolynomial.NonTorsionWeight w<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.weightedTotalDegree w p = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>w : σ → M<VAR>AddCommMonoid M<VAR>DecidableEq M<VAR>φ : MvPolynomial σ R<VAR>i : M<VAR>hi : i ∉ Finset.image (⇑(Finsupp.weight w)) φ.support<GOAL>(MvPolynomial.weightedHomogeneousComponent w i) φ = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>w : σ → M<VAR>AddCommMonoid M<VAR>DecidableEq M<VAR>φ : MvPolynomial σ R<VAR>m : M<GOAL>↑((MvPolynomial.decompose' R w φ) m) = (MvPolynomial.weightedHomogeneousComponent w m) φ
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>w : σ → M<VAR>AddCommMonoid M<VAR>DecidableEq M<GOAL>DirectSum.Decomposition.decompose' = fun φ => (DirectSum.mk (fun i => ↥(MvPolynomial.weightedHomogeneousSubmodule R w i)) (Finset.image (⇑(Finsupp.weight w)) φ.support)) fun m => ⟨(MvPolynomial.weightedHomogeneousComponent w ↑m) φ, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>σ : Type u_3<VAR>w : σ → M<VAR>AddCommMonoid M<VAR>DecidableEq M<VAR>φ : MvPolynomial σ R<VAR>m : M<GOAL>↑((DirectSum.Decomposition.decompose' φ) m) = (MvPolynomial.weightedHomogeneousComponent w m) φ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.EssFiniteType R S<GOAL>∃ s, IsLocalization (Submonoid.comap (algebraMap (↥(Algebra.adjoin R ↑s)) S) (IsUnit.submonoid S)) S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.EssFiniteType R S<GOAL>Algebra.adjoin R {x | ↑x ∈ Algebra.EssFiniteType.finset R S} = ⊤
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>σ : Finset S<GOAL>IsLocalization (Submonoid.comap (algebraMap (↥(Algebra.adjoin R ↑σ)) S) (IsUnit.submonoid S)) S ↔ ∀ (s : S), ∃ t ∈ Algebra.adjoin R ↑σ, IsUnit t ∧ s * t ∈ Algebra.adjoin R ↑σ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>Algebra.EssFiniteType R S ↔ ∃ σ, ∀ (s : S), ∃ t ∈ Algebra.adjoin R ↑σ, IsUnit t ∧ s * t ∈ Algebra.adjoin R ↑σ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Submonoid R<VAR>IsLocalization M S<GOAL>Algebra.EssFiniteType R S
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Algebra.EssFiniteType R R
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>σ : Subalgebra R S<VAR>hσ : ∀ (s : S), ∃ t ∈ σ, IsUnit t ∧ s * t ∈ σ<VAR>τ : Set T<VAR>t : T<VAR>ht : t ∈ Algebra.adjoin S τ<GOAL>∃ s ∈ σ, IsUnit s ∧ s • t ∈ Subalgebra.map (IsScalarTower.toAlgHom R S T) σ ⊔ Algebra.adjoin R τ
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>h₁ : Algebra.EssFiniteType R S<VAR>h₂ : Algebra.EssFiniteType S T<GOAL>Algebra.EssFiniteType R T
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>Algebra.EssFiniteType R S ↔ ∃ S₀ M, Algebra.FiniteType R ↥S₀ ∧ IsLocalization M S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>h : Algebra.EssFiniteType R T<GOAL>Algebra.EssFiniteType S T
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Algebra.EssFiniteType R S<GOAL>Algebra.EssFiniteType R T ↔ Algebra.EssFiniteType S T
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra.EssFiniteType R S<VAR>f g : S →ₐ[R] T<VAR>H : ∀ s ∈ Algebra.EssFiniteType.finset R S, f s = g s<GOAL>f = g
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>hpos : 0 < n<GOAL>IsIntegral ℤ μ
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<GOAL>minpoly ℤ μ ∣ Polynomial.X ^ n - 1
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<GOAL>(Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<GOAL>Squarefree (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>p : ℕ<VAR>hdiv : ¬p ∣ n<GOAL>minpoly ℤ μ ∣ (Polynomial.expand ℤ p) (minpoly ℤ (μ ^ p))
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>p : ℕ<VAR>hprime : Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<GOAL>Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) ^ p
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>p : ℕ<VAR>Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<GOAL>Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p))
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>p : ℕ<VAR>hprime : Fact (Nat.Prime p)<VAR>hdiv : ¬p ∣ n<GOAL>minpoly ℤ μ = minpoly ℤ (μ ^ p)
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>m : ℕ<VAR>hcop : m.Coprime n<GOAL>minpoly ℤ μ = minpoly ℤ (μ ^ m)
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>m : ℕ<VAR>hcop : m.Coprime n<GOAL>(Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<VAR>DecidableEq K<GOAL>primitiveRoots n K ⊆ (Polynomial.map (Int.castRingHom K) (minpoly ℤ μ)).roots.toFinset
<VAR>n : ℕ<VAR>K : Type u_1<VAR>CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>IsDomain K<VAR>CharZero K<GOAL>n.totient ≤ (minpoly ℤ μ).natDegree
<VAR>R : Type u_1<VAR>CommRing R<VAR>self : Ring.DimensionLEOne R<VAR>p : Ideal R<GOAL>p ≠ ⊥ → p.IsPrime → p.IsMaximal
<VAR>R : Type u_4<VAR>CommRing R<VAR>Ring.DimensionLEOne R<VAR>p : Ideal R<VAR>h : p.IsPrime<VAR>hp : p ≠ ⊥<GOAL>p.IsMaximal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>B : Type u_4<VAR>CommRing B<VAR>IsDomain B<VAR>Nontrivial R<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra B A<VAR>IsScalarTower R B A<VAR>IsIntegralClosure B R A<VAR>Ring.DimensionLEOne R<GOAL>Ring.DimensionLEOne B
<VAR>R : Type u_1<VAR>CommRing R<VAR>Ring.DimensionLEOne R<VAR>p₀ p₁ p₂ : Ideal R<VAR>hp₁ : p₁.IsPrime<VAR>hp₂ : p₂.IsPrime<GOAL>¬(p₀ < p₁ ∧ p₁ < p₂)
<VAR>R : Type u_1<VAR>CommRing R<VAR>Ring.DimensionLEOne R<VAR>p P : Ideal R<VAR>p.IsPrime<VAR>P.IsPrime<VAR>hpP : p < P<GOAL>p = ⊥
<VAR>A : Type u_2<VAR>CommRing A<VAR>K : Type u_4<VAR>CommRing K<VAR>Algebra A K<VAR>IsFractionRing A K<GOAL>IsDedekindRing A ↔ IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, (algebraMap A K) y = x
<VAR>A : Type u_2<VAR>CommRing A<VAR>K : Type u_4<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<GOAL>IsDedekindDomain A ↔ IsDomain A ∧ IsNoetherianRing A ∧ Ring.DimensionLEOne A ∧ ∀ {x : K}, IsIntegral A x → ∃ y, (algebraMap A K) y = x
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>k : ℕ<VAR>t : Finset σ × σ<GOAL>t ∈ MvPolynomial.NewtonIdentities.pairs σ k ↔ t.1.card ≤ k ∧ (t.1.card = k → t.2 ∈ t.1)
<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>t : Finset σ × σ<GOAL>MvPolynomial.NewtonIdentities.pairMap σ t ≠ t
<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>t : Finset σ × σ<VAR>h : t.2 ∈ t.1<GOAL>MvPolynomial.NewtonIdentities.pairMap σ t = (t.1.erase t.2, t.2)
<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>t : Finset σ × σ<VAR>h : t.2 ∉ t.1<GOAL>MvPolynomial.NewtonIdentities.pairMap σ t = (Finset.cons t.2 t.1 h, t.2)
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>k : ℕ<VAR>t : Finset σ × σ<VAR>h : t ∈ MvPolynomial.NewtonIdentities.pairs σ k<GOAL>MvPolynomial.NewtonIdentities.pairMap σ t ∈ MvPolynomial.NewtonIdentities.pairs σ k
<VAR>σ : Type u_1<VAR>DecidableEq σ<GOAL>Function.Involutive (MvPolynomial.NewtonIdentities.pairMap σ)
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<VAR>t : Finset σ × σ<VAR>h : t ∈ MvPolynomial.NewtonIdentities.pairs σ k<GOAL>MvPolynomial.NewtonIdentities.weight σ R k t + MvPolynomial.NewtonIdentities.weight σ R k (MvPolynomial.NewtonIdentities.pairMap σ t) = 0
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<GOAL>∑ t ∈ MvPolynomial.NewtonIdentities.pairs σ k, MvPolynomial.NewtonIdentities.weight σ R k t = 0
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∑ t ∈ Finset.filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k), f t = ∑ A ∈ Finset.powersetCard k Finset.univ, ∑ j ∈ A, f (A, j)
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ Finset.filter (fun a => a.1 < k) (Finset.antidiagonal k)<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∑ t ∈ Finset.filter (fun t => t.1.card = a.1) (MvPolynomial.NewtonIdentities.pairs σ k), f t = ∑ A ∈ Finset.powersetCard a.1 Finset.univ, ∑ j : σ, f (A, j)
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>k : ℕ<GOAL>Finset.filter (fun x => match x with | (s, snd) => s.card < k) (MvPolynomial.NewtonIdentities.pairs σ k) = (Finset.range k).disjiUnion (fun x => Finset.powersetCard x Finset.univ) ⋯ ×ˢ Finset.univ
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<VAR>f : Finset σ × σ → MvPolynomial σ R<GOAL>∑ t ∈ Finset.filter (fun t => t.1.card < k) (MvPolynomial.NewtonIdentities.pairs σ k), f t = ∑ a ∈ Finset.filter (fun a => a.1 < k) (Finset.antidiagonal k), ∑ A ∈ Finset.powersetCard a.1 Finset.univ, ∑ j : σ, f (A, j)
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>k : ℕ<GOAL>Disjoint (Finset.filter (fun t => t.1.card < k) (MvPolynomial.NewtonIdentities.pairs σ k)) (Finset.filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k))
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>k : ℕ<GOAL>(Finset.filter (fun t => t.1.card < k) (MvPolynomial.NewtonIdentities.pairs σ k)).disjUnion (Finset.filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k)) ⋯ = MvPolynomial.NewtonIdentities.pairs σ k
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<VAR>A : Finset σ<VAR>h : A ∈ Finset.powersetCard k Finset.univ<GOAL>∑ j ∈ A, MvPolynomial.NewtonIdentities.weight σ R k (A, j) = ↑k * (-1) ^ k * ∏ i ∈ A, MvPolynomial.X i
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<GOAL>↑k * MvPolynomial.esymm σ R k = (-1) ^ k * ∑ t ∈ Finset.filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k), MvPolynomial.NewtonIdentities.weight σ R k t
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<VAR>a : ℕ × ℕ<VAR>ha : a ∈ Finset.antidiagonal k<GOAL>∑ A ∈ Finset.powersetCard a.1 Finset.univ, ∑ j : σ, MvPolynomial.NewtonIdentities.weight σ R k (A, j) = (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>DecidableEq σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<GOAL>∑ a ∈ Finset.filter (fun a => a.1 < k) (Finset.antidiagonal k), (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2 = ∑ t ∈ Finset.filter (fun t => t.1.card < k) (MvPolynomial.NewtonIdentities.pairs σ k), MvPolynomial.NewtonIdentities.weight σ R k t
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<GOAL>↑k * MvPolynomial.esymm σ R k = (-1) ^ (k + 1) * ∑ a ∈ Finset.filter (fun a => a.1 < k) (Finset.antidiagonal k), (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>R : Type u_2<VAR>CommRing R<GOAL>∑ a ∈ Finset.antidiagonal (Fintype.card σ), (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2 = 0
<VAR>σ : Type u_1<VAR>Fintype σ<VAR>R : Type u_2<VAR>CommRing R<VAR>k : ℕ<VAR>h : 0 < k<GOAL>MvPolynomial.psum σ R k = (-1) ^ (k + 1) * ↑k * MvPolynomial.esymm σ R k - ∑ a ∈ Finset.filter (fun a => a.1 ∈ Set.Ioo 0 k) (Finset.antidiagonal k), (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
<VAR>i n : ℕ<VAR>h0 : n ≠ 0<VAR>hi : i.Coprime n<GOAL>IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n))) n
<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>IsPrimitiveRoot (Complex.exp (2 * ↑Real.pi * Complex.I / ↑n)) n
<VAR>ζ : ℂ<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>IsPrimitiveRoot ζ n ↔ ∃ i < n, ∃ (_ : i.Coprime n), Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑n)) = ζ
<VAR>n : ℕ+<VAR>x : ℂˣ<GOAL>x ∈ rootsOfUnity n ℂ ↔ ∃ i < ↑n, Complex.exp (2 * ↑Real.pi * Complex.I * (↑i / ↑↑n)) = ↑x
<VAR>n : ℕ+<GOAL>Fintype.card ↥(rootsOfUnity n ℂ) = ↑n
<VAR>k : ℕ<GOAL>(primitiveRoots k ℂ).card = k.totient
<VAR>ζ : ℂ<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<VAR>hn : n ≠ 0<GOAL>‖ζ‖ = 1
<VAR>ζ : ℂ<VAR>n : ℕ<VAR>h : IsPrimitiveRoot ζ n<VAR>hn : n ≠ 0<GOAL>‖ζ‖₊ = 1
<VAR>n m : ℕ<VAR>ζ μ : ℂ<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hμ : IsPrimitiveRoot μ m<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<VAR>h : ζ.arg = μ.arg<GOAL>ζ = μ
<VAR>n : ℕ<VAR>ζ : ℂ<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hn : n ≠ 0<GOAL>ζ.arg = 0 ↔ ζ = 1
<VAR>n : ℕ<VAR>ζ : ℂ<VAR>hζ : IsPrimitiveRoot ζ n<VAR>hn : n ≠ 0<GOAL>ζ.arg = Real.pi ↔ ζ = -1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>CommSemiring C<VAR>CommSemiring D<VAR>CommSemiring E<VAR>Algebra C D<VAR>Algebra C E<VAR>Algebra D E<VAR>IsScalarTower C D E<VAR>S : Set E<GOAL>Subalgebra.restrictScalars C (Algebra.adjoin D S) = Subalgebra.restrictScalars C (Algebra.adjoin (↥(Subalgebra.map (IsScalarTower.toAlgHom C D E) ⊤)) S)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>CommSemiring C<VAR>CommSemiring D<VAR>CommSemiring E<VAR>CommSemiring F<VAR>Algebra C D<VAR>Algebra C E<VAR>Algebra C F<VAR>Algebra D F<VAR>Algebra E F<VAR>IsScalarTower C D F<VAR>IsScalarTower C E F<VAR>S : Set D<VAR>T : Set E<VAR>hS : Algebra.adjoin C S = ⊤<VAR>hT : Algebra.adjoin C T = ⊤<GOAL>Subalgebra.restrictScalars C (Algebra.adjoin E (⇑(algebraMap D F) '' S)) = Subalgebra.restrictScalars C (Algebra.adjoin D (⇑(algebraMap E F) '' T))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra S A<VAR>Algebra R A<VAR>IsScalarTower R S A<VAR>hRS : ⊤.FG<VAR>hSA : ⊤.FG<GOAL>⊤.FG
<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>CommSemiring A<VAR>CommSemiring B<VAR>Semiring C<VAR>Algebra A B<VAR>Algebra B C<VAR>Algebra A C<VAR>IsScalarTower A B C<VAR>hAC : ⊤.FG<VAR>hBC : ⊤.FG<GOAL>∃ B₀, B₀.FG ∧ ⊤.FG
<VAR>A : Type w<VAR>B : Type u₁<VAR>C : Type u_1<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra A B<VAR>Algebra B C<VAR>Algebra A C<VAR>IsScalarTower A B C<VAR>IsNoetherianRing A<VAR>hAC : ⊤.FG<VAR>hBC : ⊤.FG<VAR>hBCi : Function.Injective ⇑(algebraMap B C)<GOAL>⊤.FG
<VAR>R : Type u<VAR>Semiring R<VAR>self : OrzechProperty R<VAR>M : Type u<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<VAR>N : Submodule R M<VAR>f : ↥N →ₗ[R] M<GOAL>Function.Surjective ⇑f → Function.Injective ⇑f
<VAR>R : Type u<VAR>Semiring R<GOAL>OrzechProperty R ↔ ∀ {M : Type u} [inst : AddCommMonoid M] [inst_1 : Module R M] [inst_2 : Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
<VAR>R : Type u<VAR>Semiring R<VAR>OrzechProperty R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<VAR>N : Type w<VAR>AddCommMonoid N<VAR>Module R N<VAR>i f : N →ₗ[R] M<VAR>hi : Function.Injective ⇑i<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective ⇑f
<VAR>R : Type u<VAR>Semiring R<VAR>OrzechProperty R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<VAR>N : Submodule R M<VAR>f : ↥N →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective ⇑f
<VAR>R : Type u<VAR>Semiring R<VAR>OrzechProperty R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective ⇑f
<VAR>R : Type u<VAR>Semiring R<VAR>OrzechProperty R<VAR>M : Type v<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Bijective ⇑f
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<GOAL>MvPolynomial.weightedTotalDegree 1 φ = φ.totalDegree