ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>p : Ideal R<VAR>IsDedekindDomain S<VAR>Algebra R S<VAR>IsNoetherian R S<VAR>p.IsMaximal<VAR>P : { x // x ∈ (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset }<GOAL>Ideal.inertiaDeg (algebraMap R S) p ↑P ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>IsDedekindDomain S<VAR>Algebra R S<VAR>p : Ideal R<VAR>hp : Ideal.map (algebraMap R S) p ≠ ⊥<VAR>x : S<GOAL>(Ideal.Factors.piQuotientEquiv p hp) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) = fun x_1 => (Ideal.Quotient.mk (↑x_1 ^ Ideal.ramificationIdx (algebraMap R S) p ↑x_1)) x
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>IsDedekindDomain S<VAR>Algebra R S<VAR>p : Ideal R<VAR>hp : Ideal.map (algebraMap R S) p ≠ ⊥<VAR>x : R<GOAL>(Ideal.Factors.piQuotientEquiv p hp) ((algebraMap R (S ⧸ Ideal.map (algebraMap R S) p)) x) = fun x_1 => (Ideal.Quotient.mk (↑x_1 ^ Ideal.ramificationIdx (algebraMap R S) p ↑x_1)) ((algebraMap R S) x)
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>p : Ideal R<VAR>IsDedekindDomain S<VAR>Algebra R S<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>IsDedekindDomain R<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>Algebra S L<VAR>IsFractionRing S L<VAR>Algebra K L<VAR>Algebra R L<VAR>IsScalarTower R S L<VAR>IsScalarTower R K L<VAR>IsNoetherian R S<VAR>IsIntegralClosure S R L<VAR>p.IsMaximal<VAR>hp0 : p ≠ ⊥<GOAL>∑ P ∈ (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset, Ideal.ramificationIdx (algebraMap R S) p P * Ideal.inertiaDeg (algebraMap R S) p P = FiniteDimensional.finrank K L
<VAR>L : FirstOrder.Language<VAR>n : ℕ<GOAL>L.skolem₁.Functions n = L.BoundedFormula Empty (n + 1)
<VAR>L : FirstOrder.Language<GOAL>∀ (x : ℕ), L.skolem₁.Relations x = Empty
<VAR>L : FirstOrder.Language<GOAL>Cardinal.mk ((n : ℕ) × (L.sum L.skolem₁).Functions n) = Cardinal.mk ((n : ℕ) × L.BoundedFormula Empty (n + 1))
<VAR>L : FirstOrder.Language<GOAL>Cardinal.mk ((n : ℕ) × (L.sum L.skolem₁).Functions n) ≤ max Cardinal.aleph0 L.card
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>Nonempty M<VAR>L.Structure M<VAR>S : (L.sum L.skolem₁).Substructure M<GOAL>(FirstOrder.Language.LHom.sumInl.substructureReduct S).IsElementary
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>Nonempty M<VAR>L.Structure M<VAR>S : (L.sum L.skolem₁).Substructure M<GOAL>↥S.elementarySkolem₁Reduct = ↥S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>Nonempty M<VAR>L.Structure M<GOAL>∃ S, Small.{max u v, w} ↥S
<VAR>L : FirstOrder.Language<VAR>M : Type w<VAR>Nonempty M<VAR>L.Structure M<VAR>s : Set M<VAR>κ : Cardinal.{w'}<VAR>h1 : Cardinal.aleph0 ≤ κ<VAR>h2 : Cardinal.lift.{w', w} (Cardinal.mk ↑s) ≤ Cardinal.lift.{w, w'} κ<VAR>h3 : Cardinal.lift.{w', max u v} L.card ≤ Cardinal.lift.{max u v, w'} κ<VAR>h4 : Cardinal.lift.{w, w'} κ ≤ Cardinal.lift.{w', w} (Cardinal.mk M)<GOAL>∃ S, s ⊆ ↑S ∧ Cardinal.lift.{w', w} (Cardinal.mk ↥S) = Cardinal.lift.{w, w'} κ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>self : T.CompleteType α<GOAL>(L.lhomWithConstants α).onTheory T ⊆ ↑self
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>self : T.CompleteType α<GOAL>(↑self).IsMaximal
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<GOAL>FirstOrder.Language.Theory.IsMaximal ↑p
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<GOAL>(L.lhomWithConstants α).onTheory T ⊆ ↑p
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>φ : L[[α]].Sentence<GOAL>φ ∈ p ∨ FirstOrder.Language.Formula.not φ ∈ p
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>φ : L[[α]].Sentence<VAR>h : (L.lhomWithConstants α).onTheory T ⊨ᵇ φ<GOAL>φ ∈ p
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>φ : L[[α]].Sentence<GOAL>FirstOrder.Language.Formula.not φ ∈ p ↔ φ ∉ p
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ : L[[α]].Sentence<GOAL>{p | φ ∈ p}ᶜ = {p | FirstOrder.Language.Formula.not φ ∈ p}
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<GOAL>{p | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>φ : L[[α]].Sentence<GOAL>{p | φ ∈ p} = Set.univ ↔ (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>S : L[[α]].Theory<GOAL>{p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<GOAL>Nonempty (T.CompleteType α) ↔ T.IsSatisfiable
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>ι : Type u_1<VAR>S : ι → L[[α]].Theory<GOAL>⋂ i, {p | S i ⊆ ↑p} = {p | ⋃ i, S i ⊆ ↑p}
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<VAR>t : Finset L[[α]].Sentence<GOAL>List.foldr (fun x x_1 => x ⊓ x_1) ⊤ t.toList ∈ p ↔ ↑t ⊆ ↑p
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>M : Type w'<VAR>L.Structure M<VAR>Nonempty M<VAR>M ⊨ T<VAR>v : α → M<VAR>φ : L[[α]].Sentence<GOAL>φ ∈ T.typeOf v ↔ (FirstOrder.Language.Formula.equivSentence.symm φ).Realize v
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>M : Type w'<VAR>L.Structure M<VAR>Nonempty M<VAR>M ⊨ T<VAR>v : α → M<VAR>φ : L.Formula α<GOAL>FirstOrder.Language.Formula.equivSentence φ ∈ T.typeOf v ↔ φ.Realize v
<VAR>L : FirstOrder.Language<VAR>T : L.Theory<VAR>α : Type w<VAR>p : T.CompleteType α<GOAL>∃ M, p ∈ T.realizedTypes (↑M) α
<VAR>A : Type u_1<VAR>SeminormedGroup A<VAR>n : ℕ<VAR>δ : ℝ<VAR>a : A<GOAL>a ∈ approxOrderOf A n δ ↔ ∃ b, orderOf b = n ∧ a ∈ Metric.ball b δ
<VAR>A : Type u_1<VAR>SeminormedAddGroup A<VAR>n : ℕ<VAR>δ : ℝ<VAR>a : A<GOAL>a ∈ approxAddOrderOf A n δ ↔ ∃ b, addOrderOf b = n ∧ a ∈ Metric.ball b δ
<VAR>A : Type u_1<VAR>SeminormedGroup A<VAR>δ : ℕ → ℝ<VAR>a : A<GOAL>a ∈ wellApproximable A δ ↔ a ∈ Filter.blimsup (fun n => approxOrderOf A n (δ n)) Filter.atTop fun n => 0 < n
<VAR>A : Type u_1<VAR>SeminormedAddGroup A<VAR>δ : ℕ → ℝ<VAR>a : A<GOAL>a ∈ addWellApproximable A δ ↔ a ∈ Filter.blimsup (fun n => approxAddOrderOf A n (δ n)) Filter.atTop fun n => 0 < n
<VAR>A : Type u_1<VAR>SeminormedAddCommGroup A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hm : 0 < m<VAR>hmn : n.Coprime m<GOAL>(fun y => m • y) '' approxAddOrderOf A n δ ⊆ approxAddOrderOf A n (↑m * δ)
<VAR>A : Type u_1<VAR>SeminormedCommGroup A<VAR>m n : ℕ<VAR>δ : ℝ<VAR>hm : 0 < m<VAR>hmn : n.Coprime m<GOAL>(fun y => y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (↑m * δ)
<VAR>A : Type u_1<VAR>SeminormedAddCommGroup A<VAR>m : ℕ<VAR>δ : ℝ<VAR>n : ℕ<VAR>hm : 0 < m<GOAL>(fun y => m • y) '' approxAddOrderOf A (n * m) δ ⊆ approxAddOrderOf A n (↑m * δ)
<VAR>A : Type u_1<VAR>SeminormedCommGroup A<VAR>m : ℕ<VAR>δ : ℝ<VAR>n : ℕ<VAR>hm : 0 < m<GOAL>(fun y => y ^ m) '' approxOrderOf A (n * m) δ ⊆ approxOrderOf A n (↑m * δ)
<VAR>A : Type u_1<VAR>SeminormedCommGroup A<VAR>a : A<VAR>n : ℕ<VAR>δ : ℝ<VAR>han : (orderOf a).Coprime n<GOAL>a • approxOrderOf A n δ ⊆ approxOrderOf A (orderOf a * n) δ
<VAR>A : Type u_1<VAR>SeminormedAddCommGroup A<VAR>a : A<VAR>n : ℕ<VAR>δ : ℝ<VAR>han : (addOrderOf a).Coprime n<GOAL>a +ᵥ approxAddOrderOf A n δ ⊆ approxAddOrderOf A (addOrderOf a * n) δ
<VAR>A : Type u_1<VAR>SeminormedCommGroup A<VAR>a : A<VAR>n : ℕ<VAR>δ : ℝ<VAR>hn : 0 < n<VAR>han : orderOf a ^ 2 ∣ n<GOAL>a • approxOrderOf A n δ = approxOrderOf A n δ
<VAR>A : Type u_1<VAR>SeminormedAddCommGroup A<VAR>a : A<VAR>n : ℕ<VAR>δ : ℝ<VAR>hn : 0 < n<VAR>han : addOrderOf a ^ 2 ∣ n<GOAL>a +ᵥ approxAddOrderOf A n δ = approxAddOrderOf A n δ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>δ : ℕ → ℝ<VAR>hδ : Filter.Tendsto δ Filter.atTop (𝓝 0)<GOAL>(∀ᵐ (x : AddCircle T), ¬addWellApproximable (AddCircle T) δ x) ∨ ∀ᵐ (x : AddCircle T), addWellApproximable (AddCircle T) δ x
<VAR>A : Type u_1<VAR>NormedAddCommGroup A<VAR>CompactSpace A<VAR>ConnectedSpace A<VAR>MeasurableSpace A<VAR>BorelSpace A<VAR>μ : MeasureTheory.Measure A<VAR>μ.IsAddHaarMeasure<VAR>ξ : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>δ : ℝ<VAR>hδ : μ Set.univ ≤ (n + 1) • μ (Metric.closedBall 0 (δ / 2))<GOAL>∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ δ
<VAR>T : ℝ<VAR>hT : Fact (0 < T)<VAR>ξ : AddCircle T<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>∃ j ∈ Set.Icc 1 n, ‖j • ξ‖ ≤ T / ↑(n + 1)
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<GOAL>↑⋯.unit = hζ.toInteger
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<GOAL>hζ.toInteger ^ 3 = 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<GOAL>u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<GOAL>(hζ.toInteger - 1) ^ 2 = -3 * ↑⋯.unit
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<GOAL>↑⋯.unit ^ 2 = -↑⋯.unit - 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hcong : ∃ n, (hζ.toInteger - 1) ^ 2 ∣ ↑u - ↑n<GOAL>u = 1 ∨ u = -1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>x : 𝓞 K<GOAL>hζ.toInteger - 1 ∣ x ∨ hζ.toInteger - 1 ∣ x - 1 ∨ hζ.toInteger - 1 ∣ x + 1
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<GOAL>↑⋯.unit ^ 2 + ↑⋯.unit + 1 = 0
<VAR>K : Type u_1<VAR>Field K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>x : 𝓞 K<GOAL>x ^ 3 - 1 = (x - 1) * (x - ↑⋯.unit) * (x - ↑⋯.unit ^ 2)
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>x : 𝓞 K<GOAL>hζ.toInteger - 1 ∣ x * (x - 1) * (x - (↑⋯.unit + 1))
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>x : 𝓞 K<VAR>h : hζ.toInteger - 1 ∣ x - 1<GOAL>(hζ.toInteger - 1) ^ 4 ∣ x ^ 3 - 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>x : 𝓞 K<VAR>h : hζ.toInteger - 1 ∣ x + 1<GOAL>(hζ.toInteger - 1) ^ 4 ∣ x ^ 3 + 1
<VAR>K : Type u_1<VAR>Field K<VAR>NumberField K<VAR>IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>x : 𝓞 K<VAR>h : ¬hζ.toInteger - 1 ∣ x<GOAL>(hζ.toInteger - 1) ^ 4 ∣ x ^ 3 - 1 ∨ (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 + 1
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.Limits.HasZeroMorphisms V<VAR>X Y : Action V G<GOAL>Action.Hom.hom 0 = 0
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.Preadditive V<VAR>X Y : Action V G<VAR>f : X ⟶ Y<GOAL>(-f).hom = -f.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.Preadditive V<VAR>X Y : Action V G<VAR>f g : X ⟶ Y<GOAL>(f + g).hom = f.hom + g.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.Preadditive V<VAR>X Y : Action V G<VAR>ι : Type u_1<VAR>f : ι → (X ⟶ Y)<VAR>s : Finset ι<GOAL>(s.sum f).hom = ∑ i ∈ s, (f i).hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.Preadditive V<VAR>R : Type u_1<VAR>Semiring R<VAR>CategoryTheory.Linear R V<VAR>X Y : Action V G<VAR>r : R<VAR>f : X ⟶ Y<GOAL>(r • f).hom = r • f.hom
<VAR>Fq : Type u_1<VAR>Fintype Fq<VAR>Semiring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Polynomial Fq<VAR>hb : b.natDegree ≤ d<VAR>A : Fin m.succ → Polynomial Fq<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
<VAR>Fq : Type u_1<VAR>Fintype Fq<VAR>Ring Fq<VAR>d m : ℕ<VAR>hm : Fintype.card Fq ^ d ≤ m<VAR>b : Polynomial Fq<VAR>A : Fin m.succ → Polynomial Fq<VAR>hA : ∀ (i : Fin m.succ), (A i).degree < b.degree<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
<VAR>Fq : Type u_1<VAR>Fintype Fq<VAR>Field Fq<VAR>b : Polynomial Fq<VAR>hb : b ≠ 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>A : Fin (Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊).succ → Polynomial Fq<GOAL>∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>Fintype Fq<VAR>Field Fq<VAR>x y z : Polynomial Fq<VAR>a : ℤ<VAR>hxy : Polynomial.cardPowDegree (x - y) < a<VAR>hyz : Polynomial.cardPowDegree (y - z) < a<GOAL>Polynomial.cardPowDegree (x - z) < a
<VAR>Fq : Type u_1<VAR>Fintype Fq<VAR>Field Fq<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Polynomial Fq<VAR>hb : b ≠ 0<VAR>A : Fin n → Polynomial Fq<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>Fintype Fq<VAR>Field Fq<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Polynomial Fq<VAR>hb : b ≠ 0<VAR>A : Fin n → Polynomial Fq<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>Group G<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module k V<VAR>Module (MonoidAlgebra k G) V<VAR>IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>AddCommGroup W<VAR>Module k W<VAR>Module (MonoidAlgebra k G) W<VAR>IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>g : G<VAR>v : W<GOAL>(π.conjugate g) v = MonoidAlgebra.single g⁻¹ 1 • π (MonoidAlgebra.single g 1 • v)
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>Group G<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module k V<VAR>Module (MonoidAlgebra k G) V<VAR>IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>AddCommGroup W<VAR>Module k W<VAR>Module (MonoidAlgebra k G) W<VAR>IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>i : V →ₗ[MonoidAlgebra k G] W<VAR>h : ∀ (v : V), π (i v) = v<VAR>g : G<VAR>v : V<GOAL>(π.conjugate g) (i v) = v
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>Group G<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module k V<VAR>Module (MonoidAlgebra k G) V<VAR>IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>AddCommGroup W<VAR>Module k W<VAR>Module (MonoidAlgebra k G) W<VAR>IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>Fintype G<VAR>v : W<GOAL>(LinearMap.sumOfConjugates G π) v = ∑ g : G, (π.conjugate g) v
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>Group G<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module k V<VAR>Module (MonoidAlgebra k G) V<VAR>IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>AddCommGroup W<VAR>Module k W<VAR>Module (MonoidAlgebra k G) W<VAR>IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>Fintype G<VAR>v : W<GOAL>(LinearMap.sumOfConjugatesEquivariant G π) v = ∑ g : G, (π.conjugate g) v
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>Group G<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module k V<VAR>Module (MonoidAlgebra k G) V<VAR>IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>AddCommGroup W<VAR>Module k W<VAR>Module (MonoidAlgebra k G) W<VAR>IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>v : W<GOAL>(LinearMap.equivariantProjection G π) v = ⅟↑(Fintype.card G) • ∑ g : G, (π.conjugate g) v
<VAR>k : Type u<VAR>CommRing k<VAR>G : Type u<VAR>Group G<VAR>V : Type v<VAR>AddCommGroup V<VAR>Module k V<VAR>Module (MonoidAlgebra k G) V<VAR>IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>AddCommGroup W<VAR>Module k W<VAR>Module (MonoidAlgebra k G) W<VAR>IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>i : V →ₗ[MonoidAlgebra k G] W<VAR>h : ∀ (v : V), π (i v) = v<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>v : V<GOAL>(LinearMap.equivariantProjection G π) (i v) = v
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>Group G<VAR>V : Type u<VAR>AddCommGroup V<VAR>Module (MonoidAlgebra k G) V<VAR>W : Type u<VAR>AddCommGroup W<VAR>Module (MonoidAlgebra k G) W<VAR>f : V →ₗ[MonoidAlgebra k G] W<VAR>hf : LinearMap.ker f = ⊥<GOAL>∃ g, g ∘ₗ f = LinearMap.id
<VAR>k : Type u<VAR>Field k<VAR>G : Type u<VAR>Fintype G<VAR>Invertible ↑(Fintype.card G)<VAR>Group G<VAR>V : Type u<VAR>AddCommGroup V<VAR>Module (MonoidAlgebra k G) V<VAR>p : Submodule (MonoidAlgebra k G) V<GOAL>∃ q, IsCompl p q
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>A : Action V G<GOAL>A.ρ 1 = 𝟙 A.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : Grp<VAR>A : Action V (MonCat.of ↑G)<VAR>g : ↑G<GOAL>(A.ρAut g).hom = A.ρ g
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : Grp<VAR>A : Action V (MonCat.of ↑G)<VAR>g : ↑G<GOAL>(A.ρAut g).inv = A.ρ g⁻¹
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>self : M.Hom N<VAR>g : ↑G<GOAL>M.ρ g ≫ self.hom = self.hom ≫ N.ρ g
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M : Action V G<GOAL>(Action.Hom.id M).hom = 𝟙 M.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M N K : Action V G<VAR>p : M.Hom N<VAR>q : N.Hom K<GOAL>(p.comp q).hom = p.hom ≫ q.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>φ₁ φ₂ : M ⟶ N<VAR>h : φ₁.hom = φ₂.hom<GOAL>φ₁ = φ₂
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M : Action V G<GOAL>(𝟙 M).hom = 𝟙 M.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M N K : Action V G<VAR>f : M ⟶ N<VAR>g : N ⟶ K<GOAL>(f ≫ g).hom = f.hom ≫ g.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>f : M.V ≅ N.V<VAR>comm : ∀ (g : ↑G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g := by aesop_cat<GOAL>(Action.mkIso f comm).hom.hom = f.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>f : M.V ≅ N.V<VAR>comm : ∀ (g : ↑G), M.ρ g ≫ f.hom = f.hom ≫ N.ρ g := by aesop_cat<GOAL>(Action.mkIso f comm).inv.hom = f.inv
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<GOAL>∀ {X Y : Action V G} (f : X ⟶ Y) (x : CategoryTheory.SingleObj ↑G), (Action.FunctorCategoryEquivalence.functor.map f).app x = f.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M : Action V G<GOAL>∀ {X Y : CategoryTheory.SingleObj ↑G} (g : X ⟶ Y), (Action.FunctorCategoryEquivalence.functor.obj M).map g = M.ρ g
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M : Action V G<GOAL>∀ (x : CategoryTheory.SingleObj ↑G), (Action.FunctorCategoryEquivalence.functor.obj M).obj x = M.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<GOAL>∀ {X Y : CategoryTheory.SingleObj ↑G ⥤ V} (f : X ⟶ Y), (Action.FunctorCategoryEquivalence.inverse.map f).hom = f.app PUnit.unit
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>F : CategoryTheory.SingleObj ↑G ⥤ V<VAR>g : ↑G<GOAL>(Action.FunctorCategoryEquivalence.inverse.obj F).ρ g = F.map g
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>F : CategoryTheory.SingleObj ↑G ⥤ V<GOAL>(Action.FunctorCategoryEquivalence.inverse.obj F).V = F.obj PUnit.unit
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>X : Action V G<GOAL>(Action.FunctorCategoryEquivalence.unitIso.inv.app X).hom = 𝟙 X.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>X : Action V G<GOAL>(Action.FunctorCategoryEquivalence.unitIso.hom.app X).hom = 𝟙 X.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>X : CategoryTheory.SingleObj ↑G ⥤ V<GOAL>∀ (X_1 : CategoryTheory.SingleObj ↑G), (Action.FunctorCategoryEquivalence.counitIso.inv.app X).app X_1 = 𝟙 (X.obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>X : CategoryTheory.SingleObj ↑G ⥤ V<GOAL>∀ (X_1 : CategoryTheory.SingleObj ↑G), (Action.FunctorCategoryEquivalence.counitIso.hom.app X).app X_1 = 𝟙 (X.obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<GOAL>(Action.functorCategoryEquivalence V G).functor = Action.FunctorCategoryEquivalence.functor
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<GOAL>(Action.functorCategoryEquivalence V G).inverse = Action.FunctorCategoryEquivalence.inverse
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<GOAL>(Action.functorCategoryEquivalence V G).counitIso = Action.FunctorCategoryEquivalence.counitIso
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<GOAL>(Action.functorCategoryEquivalence V G).unitIso = Action.FunctorCategoryEquivalence.unitIso
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M : Action V G<GOAL>(Action.forget V G).obj M = M.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<GOAL>∀ {X Y : Action V G} (f : X ⟶ Y), (Action.forget V G).map f = f.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>f : M ≅ N<VAR>g : ↑G<GOAL>N.ρ g = ((Action.forget V G).mapIso f).conj (M.ρ g)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G H : MonCat<VAR>f : G ⟶ H<VAR>M : Action V H<GOAL>((Action.res V f).obj M).V = M.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G H : MonCat<VAR>f : G ⟶ H<GOAL>∀ {X Y : Action V H} (p : X ⟶ Y), ((Action.res V f).map p).hom = p.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G H : MonCat<VAR>f : G ⟶ H<VAR>M : Action V H<GOAL>((Action.res V f).obj M).ρ = f ≫ M.ρ
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>X : Action V G<GOAL>((Action.resId V).inv.app X).hom = 𝟙 X.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>X : Action V G<GOAL>((Action.resId V).hom.app X).hom = 𝟙 X.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G H K : MonCat<VAR>f : G ⟶ H<VAR>g : H ⟶ K<VAR>X : Action V K<GOAL>((Action.resComp V f g).inv.app X).hom = 𝟙 X.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G H K : MonCat<VAR>f : G ⟶ H<VAR>g : H ⟶ K<VAR>X : Action V K<GOAL>((Action.resComp V f g).hom.app X).hom = 𝟙 X.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>F : V ⥤ W<VAR>G : MonCat<GOAL>∀ {X Y : Action V G} (f : X ⟶ Y), ((F.mapAction G).map f).hom = F.map f.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>F : V ⥤ W<VAR>G : MonCat<VAR>M : Action V G<VAR>g : ↑G<GOAL>((F.mapAction G).obj M).ρ g = F.map (M.ρ g)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>W : Type (u + 1)<VAR>CategoryTheory.LargeCategory W<VAR>F : V ⥤ W<VAR>G : MonCat<VAR>M : Action V G<GOAL>((F.mapAction G).obj M).V = F.obj M.V
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<GOAL>IsCyclotomicExtension S A B ↔ (∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1}
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>self : IsCyclotomicExtension S A B<VAR>n : ℕ+<VAR>ha : n ∈ S<GOAL>∃ r, IsPrimitiveRoot r ↑n
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>self : IsCyclotomicExtension S A B<VAR>x : B<GOAL>x ∈ Algebra.adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1}
<VAR>S : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<GOAL>IsCyclotomicExtension S A B ↔ (∀ n ∈ S, ∃ r, IsPrimitiveRoot r ↑n) ∧ Algebra.adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} = ⊤
<VAR>n : ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<GOAL>IsCyclotomicExtension {n} A B ↔ (∃ r, IsPrimitiveRoot r ↑n) ∧ ∀ (x : B), x ∈ Algebra.adjoin A {b | b ^ ↑n = 1}
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : IsCyclotomicExtension ∅ A B<GOAL>⊥ = ⊤
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : IsCyclotomicExtension {1} A B<GOAL>⊥ = ⊤
<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>h : ⊥ = ⊤<GOAL>IsCyclotomicExtension ∅ A B