ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>f : R →+* S<GOAL>(PowerSeries.map f) PowerSeries.X = PowerSeries.X
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>φ : PowerSeries R<GOAL>PowerSeries.X ^ n ∣ φ ↔ ∀ m < n, (PowerSeries.coeff R m) φ = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>PowerSeries.X ∣ φ ↔ (PowerSeries.constantCoeff R) φ = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : PowerSeries R<VAR>a : R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) ((PowerSeries.rescale a) f) = a ^ n * (PowerSeries.coeff R n) f
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>PowerSeries.rescale 0 = (PowerSeries.C R).comp (PowerSeries.constantCoeff R)
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>(PowerSeries.rescale 0) PowerSeries.X = (PowerSeries.C R) ((PowerSeries.constantCoeff R) PowerSeries.X)
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>PowerSeries.rescale 1 = RingHom.id (PowerSeries R)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : ℕ → R<VAR>a : R<GOAL>(PowerSeries.rescale a) (PowerSeries.mk f) = PowerSeries.mk fun n => a ^ n * f n
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : PowerSeries R<VAR>a b : R<GOAL>(PowerSeries.rescale b) ((PowerSeries.rescale a) f) = (PowerSeries.rescale (a * b)) f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>a b : R<GOAL>PowerSeries.rescale (a * b) = (PowerSeries.rescale b).comp (PowerSeries.rescale a)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>DecidableEq ι<VAR>f : ι → PowerSeries R<VAR>d : ℕ<VAR>s : Finset ι<GOAL>(PowerSeries.coeff R d) (∏ j ∈ s, f j) = ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (PowerSeries.coeff R (l i)) (f i)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>k n : ℕ<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff R n) (φ ^ k) = ∑ l ∈ (Finset.range k).finsuppAntidiag n, ∏ i ∈ Finset.range k, (PowerSeries.coeff R (l i)) φ
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : PowerSeries R<GOAL>(PowerSeries.coeff R 1) (φ * ψ) = (PowerSeries.coeff R 1) φ * (PowerSeries.constantCoeff R) ψ + (PowerSeries.coeff R 1) ψ * (PowerSeries.constantCoeff R) φ
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : ℕ<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff R 1) (φ ^ n) = ↑n * (PowerSeries.coeff R 1) φ * (PowerSeries.constantCoeff R) φ ^ (n - 1)
<VAR>A : Type u_2<VAR>CommRing A<GOAL>¬IsField (PowerSeries A)
<VAR>A : Type u_2<VAR>CommRing A<VAR>a : A<GOAL>(PowerSeries.rescale a) PowerSeries.X = (PowerSeries.C A) a * PowerSeries.X
<VAR>A : Type u_2<VAR>CommRing A<GOAL>(PowerSeries.rescale (-1)) PowerSeries.X = -PowerSeries.X
<VAR>A : Type u_2<VAR>CommRing A<GOAL>PowerSeries.evalNegHom PowerSeries.X = -PowerSeries.X
<VAR>R : Type u_1<VAR>Ring R<VAR>NoZeroDivisors R<VAR>φ ψ : PowerSeries R<VAR>h : φ * ψ = 0<GOAL>φ = 0 ∨ ψ = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>(Ideal.span {PowerSeries.X}).IsPrime
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>Prime PowerSeries.X
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<GOAL>Irreducible PowerSeries.X
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>a : R<VAR>ha : a ≠ 0<GOAL>Function.Injective ⇑(PowerSeries.rescale a)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>r : R<GOAL>(PowerSeries.C R) r = (algebraMap R (PowerSeries R)) r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R (PowerSeries A)) r = (PowerSeries.C A) ((algebraMap R A) r)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<GOAL>↑φ = PowerSeries.mk φ.coeff
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) ↑φ = φ.coeff n
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : ℕ<VAR>a : R<GOAL>↑((Polynomial.monomial n) a) = (PowerSeries.monomial R n) a
<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>↑0 = 0
<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>↑1 = 1
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : Polynomial R<GOAL>↑(φ + ψ) = ↑φ + ↑ψ
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : Polynomial R<GOAL>↑(φ * ψ) = ↑φ * ↑ψ
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>a : R<GOAL>↑(Polynomial.C a) = (PowerSeries.C R) a
<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>↑Polynomial.X = PowerSeries.X
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<GOAL>(PowerSeries.constantCoeff R) ↑φ = φ.coeff 0
<VAR>R : Type u_2<VAR>CommSemiring R<GOAL>Function.Injective Coe.coe
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ ψ : Polynomial R<GOAL>↑φ = ↑ψ ↔ φ = ψ
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<GOAL>↑φ = 0 ↔ φ = 0
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<GOAL>↑φ = 1 ↔ φ = 1
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<GOAL>Polynomial.coeToPowerSeries.ringHom φ = ↑φ
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<VAR>n : ℕ<GOAL>↑(φ ^ n) = ↑φ ^ n
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<GOAL>Polynomial.eval₂ (PowerSeries.C R) PowerSeries.X φ = ↑φ
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>φ : Polynomial R<VAR>A : Type u_3<VAR>Semiring A<VAR>Algebra R A<GOAL>(Polynomial.coeToPowerSeries.algHom A) φ = (PowerSeries.map (algebraMap R A)) ↑φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>p : Polynomial R<GOAL>(algebraMap (Polynomial R) (PowerSeries A)) p = (PowerSeries.map (algebraMap R A)) ↑p
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>f : PowerSeries R<GOAL>(algebraMap (PowerSeries R) (PowerSeries A)) f = (PowerSeries.map (algebraMap R A)) f
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>Ring R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<GOAL>(HahnSeries.addVal Γ R) x = x.orderTop
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>Ring R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<VAR>hx : x ≠ 0<GOAL>(HahnSeries.addVal Γ R) x = ↑x.order
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>Ring R<VAR>IsDomain R<VAR>x : HahnSeries Γ R<VAR>g : Γ<VAR>h : x.coeff g ≠ 0<GOAL>(HahnSeries.addVal Γ R) x ≤ ↑g
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<VAR>hr : r = 0<GOAL>v.intValuationDef r = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>v.intValuationDef 0 = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<VAR>hr : r ≠ 0<GOAL>v.intValuationDef r = ↑(Multiplicative.ofAdd (-↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>v.intValuationDef x ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : ↥(nonZeroDivisors R)<GOAL>v.intValuationDef ↑x ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : ↥(nonZeroDivisors R)<GOAL>0 < v.intValuationDef ↑x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : R<GOAL>v.intValuationDef x ≤ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>v.intValuationDef r < 1 ↔ v.asIdeal ∣ Ideal.span {r}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<VAR>n : ℕ<GOAL>v.intValuationDef r ≤ ↑(Multiplicative.ofAdd (-↑n)) ↔ v.asIdeal ^ n ∣ Ideal.span {r}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>v.intValuationDef 1 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x y : R<GOAL>v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y
<VAR>a b c : ℕ<GOAL>Multiplicative.ofAdd (-↑c) ≤ max (Multiplicative.ofAdd (-↑a)) (Multiplicative.ofAdd (-↑b)) ↔ min a b ≤ c
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x y : R<GOAL>v.intValuationDef (x + y) ≤ max (v.intValuationDef x) (v.intValuationDef y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>v.intValuation r = v.intValuationDef r
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>r : R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>v.intValuation r = v.intValuationDef r
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>∃ π, v.intValuationDef π = ↑(Multiplicative.ofAdd (-1))
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<VAR>hr : r ≠ 0<VAR>hv : v.asIdeal = Ideal.span {r}<GOAL>v.intValuation r = ↑(Multiplicative.ofAdd (-1))
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : K<GOAL>v.valuation x = (v.intValuation.extendToLocalization ⋯ K) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<VAR>s : ↥(nonZeroDivisors R)<GOAL>v.valuation (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation ↑s
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>v.valuation ((algebraMap R K) r) = v.intValuation r
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>v.valuation ↑r = v.intValuationDef r
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>v.valuation ((algebraMap R K) r) ≤ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>v.valuation ((algebraMap R K) r) < 1 ↔ v.asIdeal ∣ Ideal.span {r}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>∃ π, v.valuation π = ↑(Multiplicative.ofAdd (-1))
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>Classical.choose ⋯ ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : K<GOAL>Valued.v x = v.valuation x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v<GOAL>Valued.v x = Valued.extension x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v<GOAL>x ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v ↔ Valued.v x ≤ 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v<GOAL>x ∉ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v ↔ 1 < Valued.v x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<VAR>x : K<GOAL>↑K (r • x) = r • ↑K x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>⇑(algebraMap R (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = ↑K ∘ ⇑(algebraMap R K)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<GOAL>⇑(algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) = ↑K
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>Valued.v ↑r = v.valuation ↑r
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>k : K<GOAL>Valued.v (↑K k) = v.valuation k
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<GOAL>↑r ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>r : R<VAR>x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)<GOAL>↑(r • x) = r • ↑x
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>a : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v<GOAL>∃ b ∈ nonZeroDivisors R, a * ↑b ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v
<VAR>M : Type u_1<VAR>CancelMonoidWithZero M<VAR>Finite M<VAR>a : M<VAR>ha : a ≠ 0<GOAL>Function.Bijective fun b => a * b
<VAR>M : Type u_1<VAR>CancelMonoidWithZero M<VAR>Finite M<VAR>a : M<VAR>ha : a ≠ 0<GOAL>Function.Bijective fun b => b * a
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>IsDomain R<VAR>GCDMonoid R<VAR>Unique Rˣ<VAR>a b c : R<VAR>n : ℕ<VAR>cp : IsCoprime a b<VAR>h : a * b = c ^ n<GOAL>∃ d, a = d ^ n
<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>IsDomain R<VAR>GCDMonoid R<VAR>Unique Rˣ<VAR>n : ℕ<VAR>c : R<VAR>s : Finset ι<VAR>f : ι → R<VAR>h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)<VAR>hprod : ∏ i ∈ s, f i = c ^ n<VAR>i : ι<GOAL>i ∈ s → ∃ d, f i = d ^ n
<VAR>R : Type u_3<VAR>CommRing R<VAR>IsDomain R<VAR>Finite R<GOAL>IsField R
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>Group G<VAR>Fintype G<VAR>DecidableEq G<VAR>f : G →* R<VAR>hf : Function.Injective ⇑f<VAR>n : ℕ<VAR>hn : 0 < n<VAR>g₀ : G<GOAL>(Finset.filter (fun g => g ^ n = g₀) Finset.univ).card ≤ Multiset.card (Polynomial.nthRoots n (f g₀))
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>Group G<VAR>Finite G<VAR>f : G →* R<VAR>hf : Function.Injective ⇑f<GOAL>IsCyclic G
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>K : Type<VAR>Field K<VAR>Algebra (Polynomial R) K<VAR>IsFractionRing (Polynomial R) K<VAR>f : Polynomial R<VAR>g : Polynomial R<VAR>hg : g.Monic<GOAL>∃ q r, r.degree < g.degree ∧ (algebraMap (Polynomial R) K) f / (algebraMap (Polynomial R) K) g = (algebraMap (Polynomial R) K) q + (algebraMap (Polynomial R) K) r / (algebraMap (Polynomial R) K) g
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>Group G<VAR>Fintype G<VAR>f : G →* R<VAR>hf : f ≠ 1<GOAL>∑ g : G, f g = 0
<VAR>R : Type u_1<VAR>G : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>Group G<VAR>Fintype G<VAR>f : G →* R<VAR>Decidable (f = 1)<GOAL>∑ g : G, f g = ↑(if f = 1 then Fintype.card G else 0)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>a : A<VAR>m : Matrix n n R<GOAL>((MatrixEquivTensor.toFunBilinear R A n) a) m = a • m.map ⇑(algebraMap R A)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>a : A<VAR>m : Matrix n n R<GOAL>(MatrixEquivTensor.toFunAlgHom R A n) (a ⊗ₜ[R] m) = a • m.map ⇑(algebraMap R A)
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<GOAL>MatrixEquivTensor.invFun R A n 0 = 0
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>M N : Matrix n n A<GOAL>MatrixEquivTensor.invFun R A n (M + N) = MatrixEquivTensor.invFun R A n M + MatrixEquivTensor.invFun R A n N
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>a : A<VAR>M : Matrix n n A<GOAL>MatrixEquivTensor.invFun R A n (a • M) = a ⊗ₜ[R] 1 * MatrixEquivTensor.invFun R A n M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n R<GOAL>MatrixEquivTensor.invFun R A n (M.map ⇑(algebraMap R A)) = 1 ⊗ₜ[R] M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>M : Matrix n n A<GOAL>(MatrixEquivTensor.toFunAlgHom R A n) (MatrixEquivTensor.invFun R A n M) = M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>DecidableEq n<VAR>Fintype n<VAR>M : A ⊗[R] Matrix n n R<GOAL>MatrixEquivTensor.invFun R A n ((MatrixEquivTensor.toFunAlgHom R A n) M) = M
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>Fintype n<VAR>DecidableEq n<VAR>M : Matrix n n A<GOAL>(matrixEquivTensor R A n) M = ∑ p : n × n, M p.1 p.2 ⊗ₜ[R] Matrix.stdBasisMatrix p.1 p.2 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>Fintype n<VAR>DecidableEq n<VAR>i j : n<VAR>x : A<GOAL>(matrixEquivTensor R A n) (Matrix.stdBasisMatrix i j x) = x ⊗ₜ[R] Matrix.stdBasisMatrix i j 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>A : Type v<VAR>Semiring A<VAR>Algebra R A<VAR>n : Type w<VAR>Fintype n<VAR>DecidableEq n<VAR>a : A<VAR>M : Matrix n n R<GOAL>(matrixEquivTensor R A n).symm (a ⊗ₜ[R] M) = M.map fun x => a * (algebraMap R A) x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>self : Coalgebra R A<GOAL>LinearMap.lTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = (TensorProduct.mk R A R).flip 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>self : Coalgebra R A<GOAL>LinearMap.rTensor A Coalgebra.counit ∘ₗ Coalgebra.comul = (TensorProduct.mk R R A) 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>self : Coalgebra R A<GOAL>↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A Coalgebra.comul ∘ₗ Coalgebra.comul = LinearMap.lTensor A Coalgebra.comul ∘ₗ Coalgebra.comul
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>a : A<GOAL>(TensorProduct.assoc R A A A) ((LinearMap.rTensor A Coalgebra.comul) (Coalgebra.comul a)) = (LinearMap.lTensor A Coalgebra.comul) (Coalgebra.comul a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>a : A<GOAL>(TensorProduct.assoc R A A A).symm ((LinearMap.lTensor A Coalgebra.comul) (Coalgebra.comul a)) = (LinearMap.rTensor A Coalgebra.comul) (Coalgebra.comul a)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<GOAL>↑(TensorProduct.assoc R A A A).symm ∘ₗ LinearMap.lTensor A Coalgebra.comul ∘ₗ Coalgebra.comul = LinearMap.rTensor A Coalgebra.comul ∘ₗ Coalgebra.comul
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>a : A<GOAL>(LinearMap.rTensor A Coalgebra.counit) (Coalgebra.comul a) = 1 ⊗ₜ[R] a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>a : A<GOAL>(LinearMap.lTensor A Coalgebra.counit) (Coalgebra.comul a) = a ⊗ₜ[R] 1
<VAR>R : Type u<VAR>CommSemiring R<VAR>r : R<GOAL>Coalgebra.comul r = 1 ⊗ₜ[R] r
<VAR>R : Type u<VAR>CommSemiring R<VAR>r : R<GOAL>Coalgebra.counit r = r
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>Coalgebra R A<VAR>Coalgebra R B<VAR>r : A × B<GOAL>Coalgebra.comul r = (TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B)) (Coalgebra.comul r.1) + (TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B)) (Coalgebra.comul r.2)
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>Coalgebra R A<VAR>Coalgebra R B<VAR>r : A × B<GOAL>Coalgebra.counit r = Coalgebra.counit r.1 + Coalgebra.counit r.2
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>Coalgebra R A<VAR>Coalgebra R B<GOAL>Coalgebra.comul ∘ₗ LinearMap.inl R A B = TensorProduct.map (LinearMap.inl R A B) (LinearMap.inl R A B) ∘ₗ Coalgebra.comul
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>Coalgebra R A<VAR>Coalgebra R B<GOAL>Coalgebra.comul ∘ₗ LinearMap.inr R A B = TensorProduct.map (LinearMap.inr R A B) (LinearMap.inr R A B) ∘ₗ Coalgebra.comul
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>Coalgebra R A<VAR>Coalgebra R B<GOAL>Coalgebra.comul ∘ₗ LinearMap.fst R A B = TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ Coalgebra.comul
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>Coalgebra R A<VAR>Coalgebra R B<GOAL>Coalgebra.comul ∘ₗ LinearMap.snd R A B = TensorProduct.map (LinearMap.snd R A B) (LinearMap.snd R A B) ∘ₗ Coalgebra.comul
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>Coalgebra R A<VAR>Coalgebra R B<GOAL>Coalgebra.counit ∘ₗ LinearMap.inr R A B = Coalgebra.counit
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>Coalgebra R A<VAR>Coalgebra R B<GOAL>Coalgebra.counit ∘ₗ LinearMap.inl R A B = Coalgebra.counit
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>i : ι<VAR>a : A<GOAL>Coalgebra.comul (Finsupp.single i a) = (TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i)) (Coalgebra.comul a)
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>i : ι<VAR>a : A<GOAL>Coalgebra.counit (Finsupp.single i a) = Coalgebra.counit a
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>i : ι<GOAL>Coalgebra.comul ∘ₗ Finsupp.lsingle i = TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i) ∘ₗ Coalgebra.comul
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>i : ι<GOAL>Coalgebra.comul ∘ₗ Finsupp.lapply i = TensorProduct.map (Finsupp.lapply i) (Finsupp.lapply i) ∘ₗ Coalgebra.comul
<VAR>R : Type u<VAR>ι : Type v<VAR>A : Type w<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>i : ι<GOAL>Coalgebra.counit ∘ₗ Finsupp.lsingle i = Coalgebra.counit
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Coalgebra.comul = ↑(TensorProduct.tensorTensorTensorComm R A A B B) ∘ₗ TensorProduct.map Coalgebra.comul Coalgebra.comul
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Coalgebra.counit = LinearMap.mul' R R ∘ₗ TensorProduct.map Coalgebra.counit Coalgebra.counit