ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring A<VAR>Algebra R A<VAR>a : A<VAR>p : MvPolynomial σ R<GOAL>(MvPolynomial.algebraTensorAlgEquiv R A) (a ⊗ₜ[R] p) = a • (MvPolynomial.map (algebraMap R A)) p
<VAR>R : Type u<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring A<VAR>Algebra R A<VAR>s : σ<GOAL>(MvPolynomial.algebraTensorAlgEquiv R A).symm (MvPolynomial.X s) = 1 ⊗ₜ[R] MvPolynomial.X s
<VAR>R : Type u<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring A<VAR>Algebra R A<VAR>m : σ →₀ ℕ<VAR>a : A<GOAL>(MvPolynomial.algebraTensorAlgEquiv R A).symm ((MvPolynomial.monomial m) a) = a ⊗ₜ[R] (MvPolynomial.monomial m) 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>↑(S.integer K) = {x | ∀ v ∉ S, v.valuation x ≤ 1}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>(S.integer K).toSubring = ⨅ v, ⨅ (_ : v ∉ S), v.valuation.valuationSubring.toSubring
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : ↥(S.integer K)<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>hv : v ∉ S<GOAL>v.valuation ↑x ≤ 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>↑(S.unit K) = {x | ∀ v ∉ S, v.valuation ↑x = 1}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>S.unit K = ⨅ v, ⨅ (_ : v ∉ S), v.valuation.valuationSubring.unitGroup
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : ↥(S.unit K)<VAR>v : IsDedekindDomain.HeightOneSpectrum R<VAR>hv : v ∉ S<GOAL>v.valuation ↑↑x = 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : ↥(S.unit K)<GOAL>↑↑((S.unitEquivUnitsInteger K) x) = ↑↑x
<VAR>R : Type u<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Set (IsDedekindDomain.HeightOneSpectrum R)<VAR>K : Type v<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : (↥(S.integer K))ˣ<GOAL>↑((S.unitEquivUnitsInteger K).symm x) = Units.mk0 ↑↑x ⋯
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>Field K<VAR>CommRing S<VAR>Algebra K S<VAR>x : S<VAR>hx : IsIntegral K x<GOAL>(Algebra.adjoin.powerBasis hx).dim = (minpoly K x).natDegree
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>Field K<VAR>CommRing S<VAR>Algebra K S<VAR>x : S<VAR>hx : IsIntegral K x<GOAL>(Algebra.adjoin.powerBasis hx).gen = ⟨x, ⋯⟩
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>Field K<VAR>CommRing S<VAR>Algebra K S<VAR>x : S<VAR>B : PowerBasis K S<VAR>hint : IsIntegral K x<VAR>hx : B.gen ∈ Algebra.adjoin K {x}<GOAL>(B.ofGenMemAdjoin hint hx).dim = (minpoly K x).natDegree
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>Field K<VAR>CommRing S<VAR>Algebra K S<VAR>x : S<VAR>B : PowerBasis K S<VAR>hint : IsIntegral K x<VAR>hx : B.gen ∈ Algebra.adjoin K {x}<GOAL>(B.ofGenMemAdjoin hint hx).gen = x
<VAR>S : Type u_2<VAR>CommRing S<VAR>R : Type u_3<VAR>CommRing R<VAR>Algebra R S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>IsDomain S<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>n : ℕ<VAR>i : Fin B.dim<GOAL>IsIntegral R ((B.basis.repr (B.gen ^ n)) i)
<VAR>S : Type u_2<VAR>CommRing S<VAR>R : Type u_3<VAR>CommRing R<VAR>Algebra R S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>IsDomain S<VAR>x y : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hy : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr y) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>i : Fin B.dim<GOAL>IsIntegral R ((B.basis.repr (x * y)) i)
<VAR>S : Type u_2<VAR>CommRing S<VAR>R : Type u_3<VAR>CommRing R<VAR>Algebra R S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra S A<VAR>IsScalarTower R S A<VAR>B : PowerBasis S A<VAR>hB : IsIntegral R B.gen<VAR>IsDomain S<VAR>x : A<VAR>hx : ∀ (i : Fin B.dim), IsIntegral R ((B.basis.repr x) i)<VAR>hmin : minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen)<VAR>n : ℕ<VAR>i : Fin B.dim<GOAL>IsIntegral R ((B.basis.repr (x ^ n)) i)
<VAR>K : Type u_1<VAR>S : Type u_2<VAR>Field K<VAR>CommRing S<VAR>Algebra K S<VAR>R : Type u_3<VAR>CommRing R<VAR>Algebra R S<VAR>Algebra R K<VAR>IsScalarTower R K S<VAR>B B' : PowerBasis K S<VAR>P : Polynomial R<VAR>h : (Polynomial.aeval B.gen) P = B'.gen<VAR>hB : IsIntegral R B.gen<VAR>hmin : minpoly K B.gen = Polynomial.map (algebraMap R K) (minpoly R B.gen)<VAR>i : Fin B.dim<VAR>j : Fin B'.dim<GOAL>IsIntegral R (B.basis.toMatrix (⇑B'.basis) i j)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>s ⊆ ↑(Algebra.adjoin R s)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>S : Subalgebra R A<VAR>H : s ⊆ ↑S<GOAL>Algebra.adjoin R s ≤ S
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Algebra.adjoin R s = sInf {p | s ⊆ ↑p}
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>S : Subalgebra R A<GOAL>Algebra.adjoin R s ≤ S ↔ s ⊆ ↑S
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s t : Set A<VAR>H : s ⊆ t<GOAL>Algebra.adjoin R s ≤ Algebra.adjoin R t
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>S : Subalgebra R A<VAR>h₁ : s ⊆ ↑S<VAR>h₂ : S ≤ Algebra.adjoin R s<GOAL>Algebra.adjoin R s = 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>Algebra.adjoin R ↑S = S
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>α : Type u_1<VAR>s : α → Set A<GOAL>Algebra.adjoin R (Set.iUnion s) = ⨆ i, Algebra.adjoin R (s i)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>DecidableEq A<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : { x // x ∈ s } → Finset A<GOAL>Algebra.adjoin R ↑(s.attach.biUnion f) = ⨆ x, Algebra.adjoin R ↑(f x)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>p : A → Prop<VAR>x : A<VAR>h : x ∈ Algebra.adjoin R s<VAR>mem : ∀ x ∈ s, p x<VAR>algebraMap : ∀ (r : R), p ((algebraMap R A) r)<VAR>add : ∀ (x y : A), p x → p y → p (x + y)<VAR>mul : ∀ (x y : A), p x → p y → p (x * y)<GOAL>p x
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ Algebra.adjoin R s<VAR>hb : b ∈ Algebra.adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<GOAL>p a b
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>p : ↥(Algebra.adjoin R s) → Prop<VAR>mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩<VAR>algebraMap : ∀ (r : R), p ((algebraMap R ↥(Algebra.adjoin R s)) r)<VAR>add : ∀ (x y : ↥(Algebra.adjoin R s)), p x → p y → p (x + y)<VAR>mul : ∀ (x y : ↥(Algebra.adjoin R s)), p x → p y → p (x * y)<VAR>x : ↥(Algebra.adjoin R s)<GOAL>p x
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>x : A<VAR>hx : x ∈ Algebra.adjoin R s<VAR>p : (x : A) → x ∈ Algebra.adjoin R s → Prop<VAR>mem : ∀ (x : A) (h : x ∈ s), p x ⋯<VAR>algebraMap : ∀ (r : R), p ((algebraMap R A) r) ⋯<VAR>add : ∀ (x : A) (hx : x ∈ Algebra.adjoin R s) (y : A) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ Algebra.adjoin R s) (y : A) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯<GOAL>p x hx
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Algebra.adjoin R (Subtype.val ⁻¹' s) = ⊤
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s t : Set A<GOAL>Algebra.adjoin R (s ∪ t) = Algebra.adjoin R s ⊔ Algebra.adjoin R t
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.adjoin R ∅ = ⊥
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.adjoin R Set.univ = ⊤
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Subalgebra.toSubmodule (Algebra.adjoin R s) = Submodule.span R ↑(Submonoid.closure s)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Submodule.span R s ≤ Subalgebra.toSubmodule (Algebra.adjoin R s)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>t : Submodule R A<GOAL>Subalgebra.toSubmodule (Algebra.adjoin R s) ≤ t ↔ ↑(Submonoid.closure s) ⊆ ↑t
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>hs : ↑(Submonoid.closure s) ⊆ ↑(Submodule.span R s)<GOAL>Subalgebra.toSubmodule (Algebra.adjoin R s) = Submodule.span R s
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<GOAL>Algebra.adjoin R ↑(Submodule.span R s) = Algebra.adjoin R s
<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>f : A →ₐ[R] B<VAR>s : Set A<GOAL>Algebra.adjoin R (⇑f '' s) = Subalgebra.map f (Algebra.adjoin R s)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Set A<VAR>x : A<GOAL>Algebra.adjoin R (insert x ↑(Algebra.adjoin R s)) = Algebra.adjoin R (insert x s)
<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>s : Set A<VAR>t : Set B<GOAL>Algebra.adjoin R (s ×ˢ t) ≤ (Algebra.adjoin R s).prod (Algebra.adjoin R t)
<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>s : Set A<VAR>x : A<VAR>f : A →ₗ[R] B<VAR>hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂<VAR>h : x ∈ Algebra.adjoin R s<GOAL>f x ∈ Algebra.adjoin R (⇑f '' (s ∪ {1}))
<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>s : Set A<VAR>t : Set B<GOAL>Algebra.adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) = (Algebra.adjoin R s).prod (Algebra.adjoin R t)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a b : A<VAR>s : Set A<VAR>hb : b ∈ Algebra.adjoin R s<VAR>h : ∀ b ∈ s, Commute a b<GOAL>Commute a b
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a b c : A<VAR>hc : c ∈ Algebra.adjoin R {b}<VAR>h : Commute a b<GOAL>Commute a c
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>a b : A<VAR>hb : b ∈ Algebra.adjoin R {a}<GOAL>Commute a b
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>Algebra.adjoin R {1} = ⊥
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>x : A<GOAL>x ∈ Algebra.adjoin R {x}
<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>s : Set S<GOAL>Algebra.adjoin R (⇑(algebraMap S A) '' s) = Subalgebra.map (IsScalarTower.toAlgHom R S A) (Algebra.adjoin R s)
<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>s : Set S<VAR>t : Set A<GOAL>Algebra.adjoin R (⇑(algebraMap S A) '' s ∪ t) = Subalgebra.restrictScalars R (Algebra.adjoin (↥(Algebra.adjoin R s)) t)
<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>s : Set A<GOAL>Algebra.adjoin S ↑(Algebra.adjoin R s) = Algebra.adjoin S s
<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 S A<VAR>t : Set A<GOAL>Algebra.adjoin (↥⊤) t = Subalgebra.restrictScalars (↥⊤) (Algebra.adjoin S t)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>s t : Set A<GOAL>Algebra.adjoin R (s ∪ t) = Subalgebra.restrictScalars R (Algebra.adjoin (↥(Algebra.adjoin R s)) t)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>s t : Set A<GOAL>Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ t)) = Subalgebra.toSubmodule (Algebra.adjoin R s) * Subalgebra.toSubmodule (Algebra.adjoin R t)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>CommSemiring B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>r : A<VAR>s : Set B<VAR>B' : Subalgebra R B<VAR>hs : r • s ⊆ ↑B'<VAR>x : B<VAR>hx : x ∈ Algebra.adjoin R s<VAR>hr : (algebraMap A B) r ∈ B'<GOAL>∃ n₀, ∀ n ≥ n₀, r ^ n • x ∈ B'
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>r : R<VAR>s : Set A<VAR>x : A<VAR>hx : x ∈ Algebra.adjoin R s<GOAL>∃ n₀, ∀ n ≥ n₀, r ^ n • x ∈ Algebra.adjoin R (r • s)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>s : Set A<VAR>x : A<GOAL>x ∈ Algebra.adjoin R s ↔ x ∈ Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)
<VAR>R : Type uR<VAR>A : Type uA<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>s : Set A<GOAL>(Algebra.adjoin R s).toSubring = Subring.closure (Set.range ⇑(algebraMap R A) ∪ s)
<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>φ : A →ₐ[R] B<VAR>s : Set A<GOAL>Subalgebra.map φ (Algebra.adjoin R s) = Algebra.adjoin R (⇑φ '' s)
<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>e : A →ₐ[R] B<VAR>x : A<GOAL>Subalgebra.map e (Algebra.adjoin R {x}) = Algebra.adjoin R {e x}
<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>φ₁ φ₂ : A →ₐ[R] B<VAR>s : Set A<VAR>h : Set.EqOn (⇑φ₁) (⇑φ₂) s<GOAL>Algebra.adjoin R s ≤ AlgHom.equalizer φ₁ φ₂
<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>s : Set A<VAR>h : Algebra.adjoin R s = ⊤<VAR>φ₁ φ₂ : A →ₐ[R] B<VAR>hs : Set.EqOn (⇑φ₁) (⇑φ₂) s<GOAL>φ₁ = φ₂
<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>φ ψ : A →ₐ[R] B<VAR>s : Set A<GOAL>Set.EqOn ⇑φ ⇑ψ ↑(Algebra.adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s
<VAR>R : Type u_1<VAR>Semiring R<VAR>s : Set R<GOAL>Algebra.adjoin ℕ s = subalgebraOfSubsemiring (Subsemiring.closure s)
<VAR>R : Type u_1<VAR>Ring R<VAR>s : Set R<GOAL>Algebra.adjoin ℤ s = subalgebraOfSubring (Subring.closure s)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>CommSemiring E<VAR>Semiring K<VAR>SMul F E<VAR>Algebra E K<VAR>Semiring F<VAR>Module F K<VAR>IsScalarTower F E K<VAR>L : Submonoid K<VAR>S : Set K<VAR>h : ↑L = ↑(Submodule.span F S)<GOAL>Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E S
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>CommSemiring E<VAR>Semiring K<VAR>SMul F E<VAR>Algebra E K<VAR>CommSemiring F<VAR>Algebra F K<VAR>IsScalarTower F E K<VAR>L : Subalgebra F K<VAR>S : Set K<VAR>h : Subalgebra.toSubmodule L = Submodule.span F S<GOAL>Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E S
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>CommSemiring E<VAR>Semiring K<VAR>SMul F E<VAR>Algebra E K<VAR>CommSemiring F<VAR>Algebra F K<VAR>IsScalarTower F E K<VAR>L : Subalgebra F K<VAR>ι : Type u_4<VAR>bL : Basis ι F ↥L<GOAL>Subalgebra.toSubmodule (Algebra.adjoin E ↑L) = Submodule.span E (Set.range fun i => ↑(bL i))
<VAR>F : Type u_4<VAR>CommSemiring F<VAR>E : Type u_5<VAR>CommSemiring E<VAR>Algebra F E<VAR>K : Subalgebra F E<VAR>S : Set E<GOAL>Subalgebra.restrictScalars F (Algebra.adjoin (↥K) S) = Algebra.adjoin F (↑K ∪ S)
<VAR>F : Type u_4<VAR>E : Type u_5<VAR>L : Type u_6<VAR>L' : Type u_7<VAR>CommSemiring F<VAR>CommSemiring L<VAR>CommSemiring L'<VAR>Semiring E<VAR>Algebra F L<VAR>Algebra L E<VAR>Algebra F L'<VAR>Algebra L' E<VAR>Algebra F E<VAR>IsScalarTower F L E<VAR>IsScalarTower F L' E<VAR>i : L ≃ₐ[F] L'<VAR>hi : ⇑(algebraMap L E) = ⇑(algebraMap L' E) ∘ ⇑i<VAR>S : Set E<GOAL>Subalgebra.restrictScalars F (Algebra.adjoin L S) = Subalgebra.restrictScalars F (Algebra.adjoin L' S)
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>Ring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R A<GOAL>Subalgebra.comap f (Subalgebra.map f S) = S ⊔ Algebra.adjoin R (⇑f ⁻¹' {0})
<VAR>R : Type uR<VAR>A : Type uA<VAR>B : Type uB<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>Ring B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>S : Subalgebra R A<VAR>h : ⇑f ⁻¹' {0} ⊆ ↑S<GOAL>Subalgebra.comap f (Subalgebra.map f S) = S
<VAR>R S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.EssFiniteType R S<GOAL>Algebra.FormallyUnramified R S ↔ ∃ t, (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (Algebra.TensorProduct.lmul' R) t = 1
<VAR>R S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.FormallyUnramified R S<VAR>Algebra.EssFiniteType R S<VAR>s : S<GOAL>(1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * Algebra.FormallyUnramified.elem R S = 0
<VAR>R S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.FormallyUnramified R S<VAR>Algebra.EssFiniteType R S<VAR>s : S<GOAL>1 ⊗ₜ[R] s * Algebra.FormallyUnramified.elem R S = s ⊗ₜ[R] 1 * Algebra.FormallyUnramified.elem R S
<VAR>R S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.EssFiniteType R S<VAR>Algebra.FormallyUnramified R S<GOAL>(Algebra.TensorProduct.lmul' R) (Algebra.FormallyUnramified.elem R S) = 1
<VAR>R S : Type u_3<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>I : Type u_2<VAR>DecidableEq I<VAR>b : Basis I R S<VAR>f : I →₀ S<VAR>x : S<VAR>a : I → I →₀ R<VAR>ha : a = fun i => b.repr (b i * x)<GOAL>(1 ⊗ₜ[R] x * f.sum fun i y => y ⊗ₜ[R] b i) = ∑ k ∈ f.support.biUnion fun i => (a i).support, (b.repr (f.sum fun i y => (a i) k • y)).sum fun j c => c • b j ⊗ₜ[R] b k
<VAR>R S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.FormallyUnramified R S<VAR>Algebra.EssFiniteType R S<VAR>Module.Free R S<GOAL>Module.Finite R S
<VAR>R S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>Algebra.FormallyUnramified R S<VAR>Algebra.EssFiniteType R S<GOAL>TensorProduct.AlgebraTensorModule.lift (↑R (Algebra.lsmul S S M).toLinearMap.flip).flip ∘ₗ Algebra.FormallyUnramified.sec R S M = LinearMap.id
<VAR>R S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>Algebra.FormallyUnramified R S<VAR>Algebra.EssFiniteType R S<VAR>Module.Flat R M<GOAL>Module.Flat S M
<VAR>R S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>Algebra.FormallyUnramified R S<VAR>Algebra.EssFiniteType R S<VAR>Module.Projective R M<GOAL>Module.Projective S M
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>self : Algebra.FinitePresentation R A<GOAL>∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>IsNoetherianRing R<GOAL>Algebra.FiniteType R A ↔ Algebra.FinitePresentation R A
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra.FinitePresentation R A<VAR>e : A ≃ₐ[R] B<GOAL>Algebra.FinitePresentation R B
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>I : Ideal A<VAR>h : I.FG<VAR>Algebra.FinitePresentation R A<GOAL>Algebra.FinitePresentation R (A ⧸ I)
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<VAR>hker : (RingHom.ker f.toRingHom).FG<VAR>Algebra.FinitePresentation R A<GOAL>Algebra.FinitePresentation R B
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>Algebra.FinitePresentation R A ↔ ∃ n I x, I.FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>Algebra.FinitePresentation R A ↔ ∃ ι x f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra.FinitePresentation R A<VAR>ι : Type v<VAR>Finite ι<GOAL>Algebra.FinitePresentation R (MvPolynomial ι A)
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>Algebra.FinitePresentation R A<VAR>Algebra.FinitePresentation A B<GOAL>Algebra.FinitePresentation R B
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>Algebra.FinitePresentation R B<VAR>Algebra.FiniteType R A<GOAL>Algebra.FinitePresentation A B
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Function.Surjective ⇑f<VAR>Algebra.FinitePresentation R A<GOAL>(RingHom.ker f.toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>CommRing B<VAR>Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<VAR>Algebra.FinitePresentation R A<VAR>Algebra.FinitePresentation R B<GOAL>(RingHom.ker f.toRingHom).FG
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>f : A →+* B<VAR>hf : f.FinitePresentation<GOAL>f.FiniteType
<VAR>A : Type u_1<VAR>CommRing A<GOAL>(RingHom.id A).FinitePresentation
<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.FinitePresentation<VAR>hg : Function.Surjective ⇑g<VAR>hker : (RingHom.ker g).FG<GOAL>(g.comp f).FinitePresentation
<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<VAR>hker : (RingHom.ker f).FG<GOAL>f.FinitePresentation
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>IsNoetherianRing A<VAR>f : A →+* B<GOAL>f.FiniteType ↔ f.FinitePresentation
<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.FinitePresentation<VAR>hf : f.FinitePresentation<GOAL>(g.comp f).FinitePresentation