ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>hg : (g.comp f).FinitePresentation<VAR>hf : f.FiniteType<GOAL>g.FinitePresentation
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : f.FinitePresentation<GOAL>f.FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>(AlgHom.id R A).FinitePresentation
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>g : B →ₐ[R] C<VAR>f : A →ₐ[R] B<VAR>hg : g.FinitePresentation<VAR>hf : f.FinitePresentation<GOAL>(g.comp f).FinitePresentation
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<VAR>hf : f.FinitePresentation<VAR>hg : Function.Surjective ⇑g<VAR>hker : (RingHom.ker g.toRingHom).FG<GOAL>(g.comp f).FinitePresentation
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<VAR>hker : (RingHom.ker f.toRingHom).FG<GOAL>f.FinitePresentation
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>IsNoetherianRing A<VAR>f : A →ₐ[R] B<GOAL>f.FiniteType ↔ f.FinitePresentation
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<VAR>h : (g.comp f).FinitePresentation<VAR>h' : f.FiniteType<GOAL>g.FinitePresentation
<VAR>R : Type u_1<VAR>Semiring R<VAR>m n : ℕ<VAR>φ : PowerSeries R<GOAL>(PowerSeries.trunc n φ).coeff m = if m < n then (PowerSeries.coeff R m) φ else 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>PowerSeries.trunc n 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>PowerSeries.trunc (n + 1) 1 = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>a : R<GOAL>PowerSeries.trunc (n + 1) ((PowerSeries.C R) a) = Polynomial.C a
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>φ ψ : PowerSeries R<GOAL>PowerSeries.trunc n (φ + ψ) = PowerSeries.trunc n φ + PowerSeries.trunc n ψ
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>PowerSeries.trunc n.succ f = PowerSeries.trunc n f + (Polynomial.monomial n) ((PowerSeries.coeff R n) f)
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>(PowerSeries.trunc (n + 1) f).natDegree < n + 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : PowerSeries R<GOAL>PowerSeries.trunc 0 f = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>(PowerSeries.trunc n f).degree < ↑n
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_2<VAR>Semiring S<VAR>s : S<VAR>G : R →+* S<VAR>n : ℕ<VAR>f : PowerSeries R<GOAL>Polynomial.eval₂ G s (PowerSeries.trunc n f) = ∑ i ∈ Finset.range n, G ((PowerSeries.coeff R i) f) * s ^ i
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<GOAL>PowerSeries.trunc (n + 2) PowerSeries.X = Polynomial.X
<VAR>R : Type u_1<VAR>Semiring R<VAR>n : ℕ<VAR>hn : 2 ≤ n<GOAL>PowerSeries.trunc n PowerSeries.X = Polynomial.X
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n m : ℕ<VAR>f : PowerSeries R<VAR>hnm : n ≤ m := by rfl<GOAL>PowerSeries.trunc n ↑(PowerSeries.trunc m f) = PowerSeries.trunc n f
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : PowerSeries R<GOAL>PowerSeries.trunc n ↑(PowerSeries.trunc n f) = PowerSeries.trunc n f
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : ℕ<VAR>f g : PowerSeries R<GOAL>PowerSeries.trunc n (↑(PowerSeries.trunc n f) * g) = PowerSeries.trunc n (f * g)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : ℕ<VAR>f g : PowerSeries R<GOAL>PowerSeries.trunc n (f * ↑(PowerSeries.trunc n g)) = PowerSeries.trunc n (f * g)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : ℕ<VAR>f g : PowerSeries R<GOAL>PowerSeries.trunc n (↑(PowerSeries.trunc n f) * ↑(PowerSeries.trunc n g)) = PowerSeries.trunc n (f * g)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>f : PowerSeries R<VAR>n a : ℕ<GOAL>PowerSeries.trunc n (↑(PowerSeries.trunc n f) ^ a) = PowerSeries.trunc n (f ^ a)
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n : ℕ<VAR>f : Polynomial R<VAR>hn : f.natDegree < n<GOAL>PowerSeries.trunc n ↑f = f
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n m : ℕ<VAR>f : PowerSeries R<VAR>h : n < m<GOAL>(PowerSeries.coeff R n) ↑(PowerSeries.trunc m f) = (PowerSeries.coeff R n) f
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>n a b : ℕ<VAR>f g : PowerSeries R<VAR>ha : n < a<VAR>hb : n < b<GOAL>(PowerSeries.coeff R n) (f * g) = (PowerSeries.coeff R n) (↑(PowerSeries.trunc a f) * ↑(PowerSeries.trunc b g))
<VAR>R : Type u_2<VAR>CommSemiring R<VAR>d n : ℕ<VAR>f g : PowerSeries R<VAR>h : d < n<GOAL>(PowerSeries.coeff R d) (f * g) = (PowerSeries.coeff R d) (↑(PowerSeries.trunc n f) * ↑(PowerSeries.trunc n g))
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.FiniteType R A<GOAL>⊤.FG
<VAR>R : Type uR<VAR>CommSemiring R<GOAL>Algebra.FiniteType R R
<VAR>R : Type uR<VAR>CommSemiring R<GOAL>Algebra.FiniteType R R[X]
<VAR>R : Type uR<VAR>CommSemiring R<VAR>ι : Type u_1<VAR>Finite ι<GOAL>Algebra.FiniteType R (FreeAlgebra R ι)
<VAR>R : Type uR<VAR>CommSemiring R<VAR>ι : Type u_1<VAR>Finite ι<GOAL>Algebra.FiniteType R (MvPolynomial ι R)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>hA : Algebra.FiniteType R A<GOAL>Algebra.FiniteType S A
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>hRA : Algebra.FiniteType R A<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<GOAL>Algebra.FiniteType R B
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Semiring A<VAR>Semiring B<VAR>Algebra R A<VAR>Algebra R B<VAR>hRA : Algebra.FiniteType R A<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.FiniteType R B
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Semiring A<VAR>Algebra R S<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>hRS : Algebra.FiniteType R S<VAR>hSA : Algebra.FiniteType S A<GOAL>Algebra.FiniteType R A
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.FiniteType R A ↔ ∃ s f, Function.Surjective ⇑f
<VAR>R : Type uR<VAR>S : Type uS<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<GOAL>Algebra.FiniteType R S ↔ ∃ s f, Function.Surjective ⇑f
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.FiniteType R A ↔ ∃ ι x f, Function.Surjective ⇑f
<VAR>R : Type uR<VAR>S : Type uS<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<GOAL>Algebra.FiniteType R S ↔ ∃ ι x f, Function.Surjective ⇑f
<VAR>R : Type uR<VAR>S : Type uS<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<GOAL>Algebra.FiniteType R S ↔ ∃ n f, Function.Surjective ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>h : Algebra.FiniteType R S<VAR>IsNoetherianRing R<GOAL>IsNoetherianRing S
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.FG ↔ Algebra.FiniteType R ↥S
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>f : A →+* B<VAR>hf : f.Finite<GOAL>f.FiniteType
<VAR>A : Type u_1<VAR>CommRing A<GOAL>(RingHom.id A).FiniteType
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>hf : f.FiniteType<VAR>hg : Function.Surjective ⇑g<GOAL>(g.comp f).FiniteType
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>f : A →+* B<VAR>hf : Function.Surjective ⇑f<GOAL>f.FiniteType
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>g : B →+* C<VAR>f : A →+* B<VAR>hg : g.FiniteType<VAR>hf : f.FiniteType<GOAL>(g.comp f).FiniteType
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>h : (g.comp f).FiniteType<GOAL>g.FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : f.Finite<GOAL>f.FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>(AlgHom.id R A).FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>g : B →ₐ[R] C<VAR>f : A →ₐ[R] B<VAR>hg : g.FiniteType<VAR>hf : f.FiniteType<GOAL>(g.comp f).FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<VAR>hf : f.FiniteType<VAR>hg : Function.Surjective ⇑g<GOAL>(g.comp f).FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<GOAL>f.FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommRing R<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra R C<VAR>f : A →ₐ[R] B<VAR>g : B →ₐ[R] C<VAR>h : (g.comp f).FiniteType<GOAL>g.FiniteType
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddMonoid M<VAR>f : AddMonoidAlgebra R M<GOAL>f ∈ Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑f.support)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddMonoid M<VAR>S : Set (AddMonoidAlgebra R M)<VAR>hS : Algebra.adjoin R S = ⊤<GOAL>Algebra.adjoin R (⋃ f ∈ S, AddMonoidAlgebra.of' R M '' ↑f.support) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>AddMonoid M<VAR>S : Set (AddMonoidAlgebra R M)<VAR>hS : Algebra.adjoin R S = ⊤<GOAL>Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddMonoid M<VAR>h : Algebra.FiniteType R (AddMonoidAlgebra R M)<GOAL>∃ G, Algebra.adjoin R (AddMonoidAlgebra.of' R M '' ↑G) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddMonoid M<VAR>Nontrivial R<VAR>m : M<VAR>S : Set M<GOAL>AddMonoidAlgebra.of' R M m ∈ Submodule.span R (AddMonoidAlgebra.of' R M '' S) ↔ m ∈ S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>AddMonoid M<VAR>Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : AddMonoidAlgebra.of' R M m ∈ Submodule.span R ↑(Submonoid.closure (AddMonoidAlgebra.of' R M '' S))<GOAL>m ∈ AddSubmonoid.closure S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>AddCommMonoid M<VAR>CommSemiring R<VAR>S : Set M<VAR>hS : AddSubmonoid.closure S = ⊤<GOAL>Function.Surjective ⇑(MvPolynomial.aeval fun s => AddMonoidAlgebra.of' R M ↑s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>AddMonoid M<VAR>CommSemiring R<VAR>S : Set M<VAR>hS : AddSubmonoid.closure S = ⊤<GOAL>Function.Surjective ⇑((FreeAlgebra.lift R) fun s => AddMonoidAlgebra.of' R M ↑s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>AddMonoid M<VAR>CommRing R<VAR>Nontrivial R<GOAL>Algebra.FiniteType R (AddMonoidAlgebra R M) ↔ AddMonoid.FG M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>AddMonoid M<VAR>CommRing R<VAR>Nontrivial R<VAR>h : Algebra.FiniteType R (AddMonoidAlgebra R M)<GOAL>AddMonoid.FG M
<VAR>R : Type u_1<VAR>G : Type u_3<VAR>AddCommGroup G<VAR>CommRing R<VAR>Nontrivial R<GOAL>Algebra.FiniteType R (AddMonoidAlgebra R G) ↔ AddGroup.FG G
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Monoid M<VAR>f : MonoidAlgebra R M<GOAL>f ∈ Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ↑f.support)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : Algebra.adjoin R S = ⊤<GOAL>Algebra.adjoin R (⋃ f ∈ S, ⇑(MonoidAlgebra.of R M) '' ↑f.support) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Monoid M<VAR>S : Set (MonoidAlgebra R M)<VAR>hS : Algebra.adjoin R S = ⊤<GOAL>Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ⋃ f ∈ S, ↑f.support) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>Monoid M<VAR>h : Algebra.FiniteType R (MonoidAlgebra R M)<GOAL>∃ G, Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ↑G) = ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>Monoid M<VAR>Nontrivial R<VAR>m : M<VAR>S : Set M<GOAL>(MonoidAlgebra.of R M) m ∈ Submodule.span R (⇑(MonoidAlgebra.of R M) '' S) ↔ m ∈ S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommRing R<VAR>Monoid M<VAR>Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : (MonoidAlgebra.of R M) m ∈ Submodule.span R ↑(Submonoid.closure (⇑(MonoidAlgebra.of R M) '' S))<GOAL>m ∈ Submonoid.closure S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>CommMonoid M<VAR>CommSemiring R<VAR>S : Set M<VAR>hS : Submonoid.closure S = ⊤<GOAL>Function.Surjective ⇑(MvPolynomial.aeval fun s => (MonoidAlgebra.of R M) ↑s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid M<VAR>CommSemiring R<VAR>S : Set M<VAR>hS : Submonoid.closure S = ⊤<GOAL>Function.Surjective ⇑((FreeAlgebra.lift R) fun s => (MonoidAlgebra.of R M) ↑s)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid M<VAR>CommRing R<VAR>Nontrivial R<GOAL>Algebra.FiniteType R (MonoidAlgebra R M) ↔ Monoid.FG M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Monoid M<VAR>CommRing R<VAR>Nontrivial R<VAR>h : Algebra.FiniteType R (MonoidAlgebra R M)<GOAL>Monoid.FG M
<VAR>R : Type u_1<VAR>G : Type u_3<VAR>Group G<VAR>CommRing R<VAR>Nontrivial R<GOAL>Algebra.FiniteType R (MonoidAlgebra R G) ↔ Group.FG G
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>f : M →ₗ[R] M<VAR>f_surj : Function.Surjective ⇑f<GOAL>Function.Injective ⇑f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) f.derivativeFun = (PowerSeries.coeff R (n + 1)) f * (↑n + 1)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : Polynomial R<GOAL>(↑f).derivativeFun = ↑(Polynomial.derivative f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f g : PowerSeries R<GOAL>(f + g).derivativeFun = f.derivativeFun + g.derivativeFun
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>r : R<GOAL>((PowerSeries.C R) r).derivativeFun = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>PowerSeries.trunc n f.derivativeFun = Polynomial.derivative (PowerSeries.trunc (n + 1) f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f g : Polynomial R<GOAL>(↑f * ↑g).derivativeFun = ↑f * ↑(Polynomial.derivative g) + ↑g * ↑(Polynomial.derivative f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f g : PowerSeries R<GOAL>(f * g).derivativeFun = f • g.derivativeFun + g • f.derivativeFun
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>PowerSeries.derivativeFun 1 = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>r : R<VAR>f : PowerSeries R<GOAL>(r • f).derivativeFun = r • f.derivativeFun
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>r : R<GOAL>(PowerSeries.derivative R) ((PowerSeries.C R) r) = 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) ((PowerSeries.derivative R) f) = (PowerSeries.coeff R (n + 1)) f * (↑n + 1)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : Polynomial R<GOAL>(PowerSeries.derivative R) ↑f = ↑(Polynomial.derivative f)
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>(PowerSeries.derivative R) PowerSeries.X = 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>PowerSeries.trunc n ((PowerSeries.derivative R) f) = Polynomial.derivative (PowerSeries.trunc (n + 1) f)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>PowerSeries.trunc (n - 1) ((PowerSeries.derivative R) f) = Polynomial.derivative (PowerSeries.trunc n f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>NoZeroSMulDivisors ℕ R<VAR>f g : PowerSeries R<VAR>hD : (PowerSeries.derivative R) f = (PowerSeries.derivative R) g<VAR>hc : (PowerSeries.constantCoeff R) f = (PowerSeries.constantCoeff R) g<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : (PowerSeries R)ˣ<GOAL>(PowerSeries.derivative R) ↑f⁻¹ = -↑f⁻¹ ^ 2 * (PowerSeries.derivative R) ↑f
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : PowerSeries R<VAR>Invertible f<GOAL>(PowerSeries.derivative R) ⅟f = -⅟f ^ 2 * (PowerSeries.derivative R) f
<VAR>R : Type u_1<VAR>Field R<VAR>f : PowerSeries R<GOAL>(PowerSeries.derivative R) f⁻¹ = -f⁻¹ ^ 2 * (PowerSeries.derivative R) f
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>self : Bialgebra R A<GOAL>Coalgebra.comul 1 = 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>self : Bialgebra R A<GOAL>(LinearMap.mul R A).compr₂ Coalgebra.comul = (LinearMap.mul R (A ⊗[R] A)).compl₁₂ Coalgebra.comul Coalgebra.comul
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>self : Bialgebra R A<GOAL>(LinearMap.mul R A).compr₂ Coalgebra.counit = (LinearMap.mul R R).compl₁₂ Coalgebra.counit Coalgebra.counit
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>self : Bialgebra R A<GOAL>Coalgebra.counit 1 = 1
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>a b : A<GOAL>Coalgebra.counit (a * b) = Coalgebra.counit a * Coalgebra.counit b
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>a b : A<GOAL>Coalgebra.comul (a * b) = Coalgebra.comul a * Coalgebra.comul b
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>a : A<GOAL>(Bialgebra.counitAlgHom R A) a = Coalgebra.counit a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>a : A<GOAL>(Bialgebra.comulAlgHom R A) a = Coalgebra.comul a
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>r : R<GOAL>Coalgebra.counit ((algebraMap R A) r) = r
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>r : R<GOAL>Coalgebra.comul ((algebraMap R A) r) = (algebraMap R (A ⊗[R] A)) r
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>n : ℕ<GOAL>Coalgebra.counit ↑n = ↑n
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>n : ℕ<GOAL>Coalgebra.comul ↑n = ↑n
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>a : A<VAR>n : ℕ<GOAL>Coalgebra.counit (a ^ n) = Coalgebra.counit a ^ n
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>a : A<VAR>n : ℕ<GOAL>Coalgebra.comul (a ^ n) = Coalgebra.comul a ^ n
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>C : Type u_5<VAR>CommRing C<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>Algebra.IsAlgebraic K L<GOAL>IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>C : Type u_5<VAR>CommRing C<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>Algebra.IsSeparable K L<GOAL>IsLocalization (Algebra.algebraMapSubmonoid C A⁰) L
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>C : Type u_5<VAR>CommRing C<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>IsIntegrallyClosed A<GOAL>LinearMap.range (↑A (Algebra.linearMap C L)) ≤ Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis ⋯ b))
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>ι : Type u_6<VAR>Fintype ι<VAR>DecidableEq ι<VAR>b : Basis ι K L<VAR>hb_int : ∀ (i : ι), IsIntegral A (b i)<VAR>IsIntegrallyClosed A<GOAL>Subalgebra.toSubmodule (integralClosure A L) ≤ Submodule.span A (Set.range ⇑((Algebra.traceForm K L).dualBasis ⋯ b))
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>FiniteDimensional K L<VAR>s : Finset L<GOAL>∃ y, y ≠ 0 ∧ ∀ x ∈ s, IsIntegral A (y • x)
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>FiniteDimensional K L<GOAL>∃ s b, ∀ (x : { x // x ∈ s }), IsIntegral A (b x)
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>C : Type u_5<VAR>CommRing C<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>IsNoetherianRing A<GOAL>IsNoetherian A C
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>C : Type u_5<VAR>CommRing C<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>IsNoetherianRing A<GOAL>IsNoetherianRing C
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>C : Type u_5<VAR>CommRing C<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>NoZeroSMulDivisors A L<VAR>IsPrincipalIdealRing A<GOAL>Module.Free A C
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>C : Type u_5<VAR>CommRing C<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsPrincipalIdealRing A<VAR>NoZeroSMulDivisors A L<GOAL>FiniteDimensional.finrank A C = FiniteDimensional.finrank K L
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed A<VAR>IsNoetherianRing A<GOAL>IsNoetherianRing ↥(integralClosure A L)
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>C : Type u_5<VAR>CommRing C<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>Algebra C L<VAR>IsIntegralClosure C A L<VAR>Algebra A C<VAR>IsScalarTower A C L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsDomain C<VAR>IsDedekindDomain A<GOAL>IsDedekindDomain C
<VAR>A : Type u_2<VAR>K : Type u_3<VAR>CommRing A<VAR>Field K<VAR>IsDomain A<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>L : Type u_4<VAR>Field L<VAR>Algebra K L<VAR>Algebra A L<VAR>IsScalarTower A K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsDedekindDomain A<GOAL>IsDedekindDomain ↥(integralClosure A L)