ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>I J : Ideal S<VAR>Algebra R S<VAR>hI : I.IsPrime<VAR>hIJ : I ≤ J<VAR>x : S<VAR>mem : x ∈ ↑J \ ↑I<VAR>integral : IsIntegral R x<GOAL>Ideal.comap (algebraMap R S) I < Ideal.comap (algebraMap R S) J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal S<VAR>IsDomain S<VAR>r : S<VAR>r_ne_zero : r ≠ 0<VAR>hr : r ∈ I<VAR>p : Polynomial R<VAR>p_ne_zero : p ≠ 0<VAR>hp : Polynomial.eval₂ f r p = 0<GOAL>Ideal.comap f I ≠ ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>I : Ideal S<VAR>I.IsPrime<VAR>hI : (Ideal.comap (algebraMap R S) I).IsMaximal<GOAL>I.IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : f.IsIntegral<VAR>I : Ideal S<VAR>I.IsPrime<VAR>hI : (Ideal.comap f I).IsMaximal<GOAL>I.IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>I : Ideal S<VAR>Algebra R S<VAR>IsDomain S<VAR>x : S<VAR>x_ne_zero : x ≠ 0<VAR>x_mem : x ∈ I<VAR>hx : IsAlgebraic R x<GOAL>Ideal.comap (algebraMap R S) I ≠ ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>I : Ideal S<VAR>Algebra R S<VAR>Nontrivial R<VAR>IsDomain S<VAR>x : S<VAR>x_ne_zero : x ≠ 0<VAR>x_mem : x ∈ I<VAR>hx : IsIntegral R x<GOAL>Ideal.comap (algebraMap R S) I ≠ ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>I : Ideal S<VAR>Algebra R S<VAR>Nontrivial R<VAR>IsDomain S<VAR>Algebra.IsIntegral R S<VAR>hI : Ideal.comap (algebraMap R S) I = ⊥<GOAL>I = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>I : Ideal S<VAR>hI : I.IsMaximal<GOAL>(Ideal.comap (algebraMap R S) I).IsMaximal
<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : f.IsIntegral<VAR>I : Ideal S<VAR>I.IsMaximal<GOAL>(Ideal.comap f I).IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_3<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra A S<VAR>IsScalarTower R A S<VAR>IsIntegralClosure A R S<VAR>I J : Ideal A<VAR>I.IsPrime<VAR>I_lt_J : I < J<GOAL>Ideal.comap (algebraMap R A) I < Ideal.comap (algebraMap R A) J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_3<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra A S<VAR>IsScalarTower R A S<VAR>IsIntegralClosure A R S<VAR>I : Ideal A<VAR>I.IsPrime<VAR>hI : (Ideal.comap (algebraMap R A) I).IsMaximal<GOAL>I.IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_3<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra A S<VAR>IsScalarTower R A S<VAR>IsIntegralClosure A R S<VAR>IsDomain A<VAR>Nontrivial R<VAR>I : Ideal A<VAR>I_ne_bot : I ≠ ⊥<GOAL>Ideal.comap (algebraMap R A) I ≠ ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_3<VAR>CommRing A<VAR>Algebra R A<VAR>Algebra A S<VAR>IsScalarTower R A S<VAR>IsIntegralClosure A R S<VAR>IsDomain A<VAR>Nontrivial R<VAR>I : Ideal A<GOAL>Ideal.comap (algebraMap R A) I = ⊥ → I = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I J : Ideal ↥(integralClosure R S)<VAR>I.IsPrime<VAR>I_lt_J : I < J<GOAL>Ideal.comap (algebraMap R ↥(integralClosure R S)) I < Ideal.comap (algebraMap R ↥(integralClosure R S)) J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I : Ideal ↥(integralClosure R S)<VAR>I.IsPrime<VAR>hI : (Ideal.comap (algebraMap R ↥(integralClosure R S)) I).IsMaximal<GOAL>I.IsMaximal
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain S<VAR>Nontrivial R<VAR>I : Ideal ↥(integralClosure R S)<VAR>I_ne_bot : I ≠ ⊥<GOAL>Ideal.comap (algebraMap R ↥(integralClosure R S)) I ≠ ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain S<VAR>Nontrivial R<VAR>I : Ideal ↥(integralClosure R S)<GOAL>Ideal.comap (algebraMap R ↥(integralClosure R S)) I = ⊥ → I = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsDomain S<VAR>Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>P.IsPrime<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<GOAL>∃ Q, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>P.IsPrime<VAR>I : Ideal S<VAR>I.IsPrime<VAR>hIP : Ideal.comap (algebraMap R S) I ≤ P<GOAL>∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>P : Ideal R<VAR>P.IsPrime<VAR>I : Ideal S<VAR>hI : Ideal.comap (algebraMap R S) I ≤ P<GOAL>∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q ≤ P
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>P.IsPrime<VAR>I : Ideal S<VAR>hIP : Ideal.comap (algebraMap R S) I ≤ P<GOAL>∃ Q ≥ I, Q.IsPrime ∧ Ideal.comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.IsIntegral R S<VAR>P : Ideal R<VAR>P_max : P.IsMaximal<VAR>hP : RingHom.ker (algebraMap R S) ≤ P<GOAL>∃ Q, Q.IsMaximal ∧ Ideal.comap (algebraMap R S) Q = P
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : RingHom.ker f ≤ I<VAR>hf₂ : f.IsIntegral<GOAL>Ideal.map f I = ⊤ ↔ I = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal R<VAR>hf₁ : Function.Injective ⇑f<VAR>hf₂ : f.IsIntegral<GOAL>Ideal.map f I = ⊤ ↔ I = ⊤
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>∀ (a : ↥I), I.toCotangent a = Submodule.Quotient.mk a
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>Submodule.map (Submodule.subtype I) (LinearMap.ker I.toCotangent) = I ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>x : ↥I<GOAL>x ∈ LinearMap.ker I.toCotangent ↔ ↑x ∈ I ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>x y : ↥I<GOAL>I.toCotangent x = I.toCotangent y ↔ ↑x - ↑y ∈ I ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>x : ↥I<GOAL>I.toCotangent x = 0 ↔ ↑x ∈ I ^ 2
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>Function.Surjective ⇑I.toCotangent
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>LinearMap.range I.toCotangent = ⊤
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>Subsingleton I.Cotangent ↔ IsIdempotentElem I
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.cotangentToQuotientSquare ∘ₗ I.toCotangent = Submodule.mkQ (I ^ 2) ∘ₗ Submodule.subtype I
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>x : ↥I<GOAL>I.cotangentToQuotientSquare (I.toCotangent x) = (Submodule.mkQ (I ^ 2)) ↑x
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.cotangentIdeal ^ 2 = ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>LinearMap.range I.cotangentToQuotientSquare = Submodule.restrictScalars R I.cotangentIdeal
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>x : I.Cotangent<GOAL>↑(I.cotangentEquivIdeal x) = I.cotangentToQuotientSquare x
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>x : R<VAR>hx : x ∈ I<GOAL>I.cotangentEquivIdeal.symm ⟨(Submodule.mkQ (I ^ 2)) x, ⋯⟩ = I.toCotangent ⟨x, hx⟩
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>f : A →ₐ[R] B<GOAL>RingHom.ker f.kerSquareLift.toRingHom = (RingHom.ker f.toRingHom).cotangentIdeal
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>I₁ : Ideal A<VAR>I₂ : Ideal B<VAR>f : A →ₐ[R] B<VAR>h : I₁ ≤ Ideal.comap f I₂<VAR>x : ↥I₁<GOAL>(I₁.mapCotangent I₂ f h) (I₁.toCotangent x) = I₂.toCotangent ⟨f ↑x, ⋯⟩
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>IsNoetherianRing R<GOAL>Subsingleton (LocalRing.CotangentSpace R) ↔ IsField R
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>IsNoetherianRing R<VAR>M : Submodule R ↥(LocalRing.maximalIdeal R)<GOAL>Submodule.map (LocalRing.maximalIdeal R).toCotangent M = ⊤ ↔ M = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>IsNoetherianRing R<VAR>s : Set ↥(LocalRing.maximalIdeal R)<GOAL>Submodule.span (LocalRing.ResidueField R) (⇑(LocalRing.maximalIdeal R).toCotangent '' s) = ⊤ ↔ Submodule.span R s = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>IsNoetherianRing R<GOAL>FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 0 ↔ IsField R
<VAR>R : Type u_2<VAR>Field R<GOAL>FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>IsNoetherianRing R<GOAL>FiniteDimensional.finrank (LocalRing.ResidueField R) (LocalRing.CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (LocalRing.maximalIdeal R)
<VAR>α : Type u<VAR>DecidableEq α<VAR>xs : List (α × α)<VAR>x y z : α<GOAL>SlimCheck.InjectiveFunction.List.applyId ((y, z) :: xs) x = if y = x then z else SlimCheck.InjectiveFunction.List.applyId xs x
<VAR>α : Type u<VAR>DecidableEq α<VAR>xs ys : List α<VAR>h₀ : xs.Nodup<VAR>h₁ : xs.length = ys.length<VAR>x y : α<VAR>i : ℕ<VAR>h₂ : xs[i]? = some x<GOAL>SlimCheck.InjectiveFunction.List.applyId (xs.zip ys) x = y ↔ ys[i]? = some y
<VAR>α : Type u<VAR>DecidableEq α<VAR>xs ys : List α<VAR>h₀ : xs.Nodup<VAR>h₁ : xs ~ ys<VAR>x : α<GOAL>SlimCheck.InjectiveFunction.List.applyId (xs.zip ys) x ∈ ys ↔ x ∈ xs
<VAR>α : Type u<VAR>DecidableEq α<VAR>xs ys : List α<VAR>x : α<GOAL>x ∉ xs → SlimCheck.InjectiveFunction.List.applyId (xs.zip ys) x = x
<VAR>α : Type u<VAR>DecidableEq α<VAR>xs ys : List α<VAR>h₀ : xs.Nodup<VAR>h₁ : xs ~ ys<GOAL>Function.Injective (SlimCheck.InjectiveFunction.List.applyId (xs.zip ys))
<VAR>α : Type u<VAR>DecidableEq α<VAR>f : SlimCheck.InjectiveFunction α<GOAL>Function.Injective f.apply
<VAR>R : Type u_1<VAR>CommRing R<VAR>a b : Fin 3 → R<GOAL>(crossProduct a) b = ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]
<VAR>R : Type u_1<VAR>CommRing R<VAR>v w : Fin 3 → R<GOAL>-(crossProduct v) w = (crossProduct w) v
<VAR>R : Type u_1<VAR>CommRing R<VAR>v w : Fin 3 → R<GOAL>(crossProduct v) w + (crossProduct w) v = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>v : Fin 3 → R<GOAL>(crossProduct v) v = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>v w : Fin 3 → R<GOAL>v ⬝ᵥ (crossProduct v) w = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>v w : Fin 3 → R<GOAL>w ⬝ᵥ (crossProduct v) w = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>u v w : Fin 3 → R<GOAL>u ⬝ᵥ (crossProduct v) w = v ⬝ᵥ (crossProduct w) u
<VAR>R : Type u_1<VAR>CommRing R<VAR>u v w : Fin 3 → R<GOAL>u ⬝ᵥ (crossProduct v) w = Matrix.det ![u, v, w]
<VAR>R : Type u_1<VAR>CommRing R<VAR>u v w x : Fin 3 → R<GOAL>(crossProduct u) v ⬝ᵥ (crossProduct w) x = u ⬝ᵥ w * v ⬝ᵥ x - u ⬝ᵥ x * v ⬝ᵥ w
<VAR>R : Type u_1<VAR>CommRing R<VAR>u v w : Fin 3 → R<GOAL>(crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)
<VAR>R : Type u_1<VAR>CommRing R<VAR>u v w : Fin 3 → R<GOAL>(crossProduct ((crossProduct u) v)) w = (crossProduct u) ((crossProduct v) w) - (crossProduct v) ((crossProduct u) w)
<VAR>R : Type u_1<VAR>CommRing R<VAR>u v w : Fin 3 → R<GOAL>(crossProduct u) ((crossProduct v) w) + (crossProduct v) ((crossProduct w) u) + (crossProduct w) ((crossProduct u) v) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.Generators R S<VAR>s : S<GOAL>(MvPolynomial.aeval self.val) (self.σ' s) = s
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>s : S<GOAL>(MvPolynomial.aeval P.val) (P.σ s) = s
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>algebraMap P.Ring S = ↑(MvPolynomial.aeval P.val)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x : P.Ring<GOAL>(algebraMap P.Ring S) x = (MvPolynomial.aeval P.val) x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x y : S<GOAL>P.σ x • y = x * y
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Function.Injective P.σ
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Function.Surjective ⇑(algebraMap P.Ring S)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>vars : Type u_1<VAR>val : vars → S<VAR>h : Function.Surjective ⇑(MvPolynomial.aeval val)<GOAL>(Algebra.Generators.ofSurjective val h).vars = vars
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>vars : Type u_1<VAR>val : vars → S<VAR>h : Function.Surjective ⇑(MvPolynomial.aeval val)<GOAL>∀ (a : vars), (Algebra.Generators.ofSurjective val h).val a = val a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>n : S<GOAL>(Algebra.Generators.self R S).σ n = MvPolynomial.X n
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>(Algebra.Generators.self R S).vars = S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>a : S<GOAL>(Algebra.Generators.self R S).val a = id a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<VAR>s : S<GOAL>(Algebra.Generators.localizationAway r).σ s = MvPolynomial.C (IsLocalization.Away.sec r s).1 * MvPolynomial.X () ^ (IsLocalization.Away.sec r s).2
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>∀ (x : Unit), (Algebra.Generators.localizationAway r).val x = IsLocalization.Away.invSelf r
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>IsLocalization.Away r S<GOAL>(Algebra.Generators.localizationAway r).vars = Unit
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Q : Algebra.Generators S T<VAR>P : Algebra.Generators R S<VAR>x : T<GOAL>(Q.comp P).σ x = Finsupp.sum (Q.σ x) fun n r => (MvPolynomial.rename Sum.inr) (P.σ r) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl n)) 1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Q : Algebra.Generators S T<VAR>P : Algebra.Generators R S<GOAL>∀ (a : Q.vars ⊕ P.vars), (Q.comp P).val a = Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val) a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Q : Algebra.Generators S T<VAR>P : Algebra.Generators R S<GOAL>(Q.comp P).vars = (Q.vars ⊕ P.vars)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>P : Algebra.Generators R T<GOAL>∀ (a : P.vars), (Algebra.Generators.extendScalars S P).val a = P.val a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>P : Algebra.Generators R T<GOAL>(Algebra.Generators.extendScalars S P).vars = P.vars
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>P : Algebra.Generators R S<VAR>x : P.vars<GOAL>P.baseChange.val x = 1 ⊗ₜ[R] P.val x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>P : Algebra.Generators R S<GOAL>P.baseChange.vars = P.vars
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra S S'<VAR>self : P.Hom P'<VAR>i : P.vars<GOAL>(MvPolynomial.aeval P'.val) (self.val i) = (algebraMap S S') (P.val i)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : P.Hom P'<VAR>x : P.Ring<GOAL>(MvPolynomial.aeval P'.val) (f.toAlgHom x) = (algebraMap S S') ((MvPolynomial.aeval P.val) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>f : P.Hom P'<VAR>i : P.vars<GOAL>f.toAlgHom (MvPolynomial.X i) = f.val i
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>f : P.Hom P'<VAR>r : R<GOAL>f.toAlgHom (MvPolynomial.C r) = MvPolynomial.C ((algebraMap R R') r)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>f : P.Hom P'<VAR>v : P.vars →₀ ℕ<VAR>r : R<GOAL>f.toAlgHom ((MvPolynomial.monomial v) r) = r • v.prod fun x x_1 => f.val x ^ x_1
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : P.Hom P'<GOAL>↑(Algebra.Generators.Hom.equivAlgHom f) = f.toAlgHom
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : { f // ∀ (x : P.Ring), (MvPolynomial.aeval P'.val) (f x) = (algebraMap S S') ((MvPolynomial.aeval P.val) x) }<VAR>i : P.vars<GOAL>(Algebra.Generators.Hom.equivAlgHom.symm f).val i = ↑f (MvPolynomial.X i)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra S S'<GOAL>∀ (a : P.vars), (P.defaultHom P').val a = (P'.σ ∘ ⇑(algebraMap S S') ∘ P.val) a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>n : P.vars<GOAL>(Algebra.Generators.Hom.id P).val n = MvPolynomial.X n
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>(Algebra.Generators.Hom.id P).toAlgHom = AlgHom.id R P.Ring
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra S S'<VAR>R'' : Type u_4<VAR>S'' : Type u_5<VAR>CommRing R''<VAR>CommRing S''<VAR>Algebra R'' S''<VAR>P'' : Algebra.Generators R'' S''<VAR>Algebra S S''<VAR>Algebra R' R''<VAR>Algebra S' S''<VAR>Algebra R' S''<VAR>IsScalarTower R' R'' S''<VAR>IsScalarTower R' S' S''<VAR>IsScalarTower S S' S''<VAR>f : P'.Hom P''<VAR>g : P.Hom P'<VAR>x : P.vars<GOAL>(f.comp g).val x = (MvPolynomial.aeval f.val) (g.val x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : P.Hom P'<GOAL>f.comp (Algebra.Generators.Hom.id P) = f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra S S'<VAR>f : P.Hom P'<GOAL>(Algebra.Generators.Hom.id P').comp f = f
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>R'' : Type u_4<VAR>S'' : Type u_5<VAR>CommRing R''<VAR>CommRing S''<VAR>Algebra R'' S''<VAR>P'' : Algebra.Generators R'' S''<VAR>Algebra R R''<VAR>Algebra S S''<VAR>Algebra R' R''<VAR>Algebra S' S''<VAR>Algebra R' S''<VAR>IsScalarTower R' R'' S''<VAR>IsScalarTower R' S' S''<VAR>IsScalarTower R R' R''<VAR>IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<VAR>x : P.Ring<GOAL>(g.comp f).toAlgHom x = g.toAlgHom (f.toAlgHom x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Q : Algebra.Generators S T<VAR>P : Algebra.Generators R S<VAR>i : P.vars<GOAL>(Q.toComp P).val i = MvPolynomial.X (Sum.inr i)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Q : Algebra.Generators S T<VAR>P : Algebra.Generators R S<VAR>i : (Q.comp P).vars<GOAL>(Q.ofComp P).val i = Sum.elim MvPolynomial.X (⇑MvPolynomial.C ∘ P.val) i
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>T : Type u_1<VAR>CommRing T<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>P : Algebra.Generators R T<VAR>n : P.vars<GOAL>P.toExtendScalars.val n = MvPolynomial.X n
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>P.ker = RingHom.ker (MvPolynomial.aeval P.val)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x y : P.Cotangent<VAR>e : x.val = y.val<GOAL>x = y
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x y : P.Cotangent<GOAL>(x + y).val = x.val + y.val
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Algebra.Generators.Cotangent.val 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>w z : P.ker.Cotangent<GOAL>Algebra.Generators.Cotangent.of (w + z) = Algebra.Generators.Cotangent.of w + Algebra.Generators.Cotangent.of z
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Algebra.Generators.Cotangent.of 0 = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x : P.Cotangent<GOAL>Algebra.Generators.Cotangent.of x.val = x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>w : P.ker.Cotangent<GOAL>(Algebra.Generators.Cotangent.of w).val = w
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x y : P.Cotangent<GOAL>(x - y).val = x.val - y.val
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>p : P.Ring<VAR>hp : p ∈ P.ker<VAR>m : P.ker.Cotangent<GOAL>p • m = 0