ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<GOAL>MvPolynomial.weightedHomogeneousSubmodule R 1 n = MvPolynomial.homogeneousSubmodule σ R n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<VAR>p : MvPolynomial σ R<GOAL>p ∈ MvPolynomial.homogeneousSubmodule σ R n ↔ p.IsHomogeneous n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<GOAL>MvPolynomial.homogeneousSubmodule σ R n = Finsupp.supported R R {d | d.degree = n}
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>m n : ℕ<GOAL>MvPolynomial.homogeneousSubmodule σ R m * MvPolynomial.homogeneousSubmodule σ R n ≤ MvPolynomial.homogeneousSubmodule σ R (m + n)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>d : σ →₀ ℕ<VAR>r : R<VAR>n : ℕ<VAR>hn : d.degree = n<GOAL>((MvPolynomial.monomial d) r).IsHomogeneous n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.totalDegree = 0 ↔ p.IsHomogeneous 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>r : R<GOAL>(MvPolynomial.C r).IsHomogeneous 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<GOAL>MvPolynomial.IsHomogeneous 0 n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>MvPolynomial.IsHomogeneous 1 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>i : σ<GOAL>(MvPolynomial.X i).IsHomogeneous 1
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : d.degree ≠ n<GOAL>MvPolynomial.coeff d φ = 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hm : φ.IsHomogeneous m<VAR>hn : φ.IsHomogeneous n<VAR>hφ : φ ≠ 0<GOAL>m = n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ ψ : MvPolynomial σ R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>hψ : ψ.IsHomogeneous n<GOAL>(φ + ψ).IsHomogeneous n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>φ : ι → MvPolynomial σ R<VAR>n : ℕ<VAR>h : ∀ i ∈ s, (φ i).IsHomogeneous n<GOAL>(∑ i ∈ s, φ i).IsHomogeneous n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>hψ : ψ.IsHomogeneous n<GOAL>(φ * ψ).IsHomogeneous (m + n)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>φ : ι → MvPolynomial σ R<VAR>n : ι → ℕ<VAR>h : ∀ i ∈ s, (φ i).IsHomogeneous (n i)<GOAL>(∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>m : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>r : R<GOAL>(MvPolynomial.C r * φ).IsHomogeneous m
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>r : R<VAR>i : σ<GOAL>(MvPolynomial.C r * MvPolynomial.X i).IsHomogeneous 1
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>m : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>n : ℕ<GOAL>(φ ^ n).IsHomogeneous (m * n)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>i : σ<VAR>n : ℕ<GOAL>(MvPolynomial.X i ^ n).IsHomogeneous n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>r : R<VAR>i : σ<VAR>n : ℕ<GOAL>(MvPolynomial.C r * MvPolynomial.X i ^ n).IsHomogeneous n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>φ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>f : R →+* MvPolynomial τ S<VAR>g : σ → MvPolynomial τ S<VAR>hf : ∀ (r : R), (f r).IsHomogeneous 0<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<GOAL>(MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>f : R →+* S<GOAL>((MvPolynomial.map f) φ).IsHomogeneous n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>φ : MvPolynomial σ R<VAR>m n : ℕ<VAR>Algebra R S<VAR>hφ : φ.IsHomogeneous m<VAR>g : σ → MvPolynomial τ S<VAR>hg : ∀ (i : σ), (g i).IsHomogeneous n<GOAL>((MvPolynomial.aeval g) φ).IsHomogeneous (n * m)
<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>CommRing R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<GOAL>(-φ).IsHomogeneous n
<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>CommRing R<VAR>φ ψ : MvPolynomial σ R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>hψ : ψ.IsHomogeneous n<GOAL>(φ - ψ).IsHomogeneous n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<GOAL>φ.totalDegree ≤ n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>h : φ ≠ 0<GOAL>φ.totalDegree = n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<VAR>f : σ → τ<VAR>h : φ.IsHomogeneous n<GOAL>((MvPolynomial.rename f) φ).IsHomogeneous n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<VAR>f : σ → τ<VAR>hf : Function.Injective f<GOAL>((MvPolynomial.rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>N : ℕ<VAR>φ : MvPolynomial (Fin (N + 1)) R<VAR>n : ℕ<VAR>hφ : φ.IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<GOAL>(((MvPolynomial.finSuccEquiv R N) φ).coeff i).IsHomogeneous j
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<VAR>hσ : Finite σ<VAR>p : Polynomial (MvPolynomial σ R)<VAR>hp : ((MvPolynomial.optionEquivLeft R σ).symm p).IsHomogeneous n<VAR>i j : ℕ<VAR>h : i + j = n<GOAL>(p.coeff i).IsHomogeneous j
<VAR>R : Type u_3<VAR>CommSemiring R<VAR>N : ℕ<VAR>F : MvPolynomial (Fin N.succ) R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hFn : ((MvPolynomial.finSuccEquiv R N) F).coeff n ≠ 0<GOAL>∃ r, (MvPolynomial.eval r) F ≠ 0
<VAR>R : Type u_5<VAR>CommRing R<VAR>IsDomain R<VAR>N : ℕ<VAR>F : MvPolynomial (Fin N) R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hF₀ : F ≠ 0<VAR>hnR : ↑n ≤ Cardinal.mk R<GOAL>∃ r, (MvPolynomial.eval r) F ≠ 0
<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>CommRing R<VAR>IsDomain R<VAR>F : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (MvPolynomial.eval r) F = 0<VAR>hnR : ↑n ≤ Cardinal.mk R<GOAL>F = 0
<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>CommRing R<VAR>IsDomain R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hG : G.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G<VAR>hnR : ↑n ≤ Cardinal.mk R<GOAL>F = G
<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>CommRing R<VAR>IsDomain R<VAR>Infinite R<VAR>F : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (MvPolynomial.eval r) F = 0<GOAL>F = 0
<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>CommRing R<VAR>IsDomain R<VAR>Infinite R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hG : G.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (MvPolynomial.eval r) F = (MvPolynomial.eval r) G<GOAL>F = G
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.homogeneousComponent n) φ ∈ MvPolynomial.homogeneousSubmodule σ R n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<VAR>φ : MvPolynomial σ R<VAR>d : σ →₀ ℕ<GOAL>MvPolynomial.coeff d ((MvPolynomial.homogeneousComponent n) φ) = if d.degree = n then MvPolynomial.coeff d φ else 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.homogeneousComponent n) φ = ∑ d ∈ Finset.filter (fun d => d.degree = n) φ.support, (MvPolynomial.monomial d) (MvPolynomial.coeff d φ)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<VAR>φ : MvPolynomial σ R<GOAL>((MvPolynomial.homogeneousComponent n) φ).IsHomogeneous n
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<GOAL>(MvPolynomial.homogeneousComponent 0) φ = MvPolynomial.C (MvPolynomial.coeff 0 φ)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>n : ℕ<VAR>r : R<GOAL>(MvPolynomial.homogeneousComponent n) (MvPolynomial.C r * φ) = MvPolynomial.C r * (MvPolynomial.homogeneousComponent n) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<VAR>φ : MvPolynomial σ R<VAR>h : ∀ d ∈ φ.support, d.degree ≠ n<GOAL>(MvPolynomial.homogeneousComponent n) φ = 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>n : ℕ<VAR>φ : MvPolynomial σ R<VAR>h : φ.totalDegree < n<GOAL>(MvPolynomial.homogeneousComponent n) φ = 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<GOAL>∑ i ∈ Finset.range (φ.totalDegree + 1), (MvPolynomial.homogeneousComponent i) φ = φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>m n : ℕ<VAR>p : MvPolynomial σ R<VAR>h : p ∈ MvPolynomial.homogeneousSubmodule σ R n<GOAL>(MvPolynomial.homogeneousComponent m) p = if m = n then p else 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>SetLike.GradedMonoid (MvPolynomial.homogeneousSubmodule σ R)
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>φ : MvPolynomial σ R<VAR>i : ℕ<GOAL>↑((DirectSum.Decomposition.decompose' φ) i) = (MvPolynomial.homogeneousComponent i) φ
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<GOAL>DirectSum.Decomposition.decompose' = fun φ => (DirectSum.mk (fun i => ↥(MvPolynomial.homogeneousSubmodule σ R i)) (Finset.image Finsupp.degree φ.support)) fun m => ⟨(MvPolynomial.homogeneousComponent ↑m) φ, ⋯⟩
<VAR>A : Type u<VAR>B : Type v<VAR>ι : Type w<VAR>DecidableEq ι<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Fintype ι<VAR>b : ι → B<GOAL>Algebra.discr A b = (Algebra.traceMatrix A b).det
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>DecidableEq ι<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>CommRing C<VAR>Algebra A C<VAR>Fintype ι<VAR>b : ι → B<VAR>f : B ≃ₐ[A] C<GOAL>Algebra.discr A b = Algebra.discr A (⇑f ∘ b)
<VAR>A : Type u<VAR>B : Type v<VAR>ι : Type w<VAR>DecidableEq ι<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>ι' : Type u_1<VAR>Fintype ι'<VAR>Fintype ι<VAR>DecidableEq ι'<VAR>b : Basis ι A B<VAR>f : ι ≃ ι'<GOAL>Algebra.discr A (⇑b ∘ ⇑f.symm) = Algebra.discr A ⇑b
<VAR>A : Type u<VAR>B : Type v<VAR>ι : Type w<VAR>DecidableEq ι<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Fintype ι<VAR>IsDomain A<VAR>b : ι → B<VAR>hli : ¬LinearIndependent A b<GOAL>Algebra.discr A b = 0
<VAR>A : Type u<VAR>B : Type v<VAR>ι : Type w<VAR>DecidableEq ι<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Fintype ι<VAR>b : ι → B<VAR>P : Matrix ι ι A<GOAL>Algebra.discr A (b ᵥ* P.map ⇑(algebraMap A B)) = P.det ^ 2 * Algebra.discr A b
<VAR>A : Type u<VAR>B : Type v<VAR>ι : Type w<VAR>DecidableEq ι<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Fintype ι<VAR>b : ι → B<VAR>P : Matrix ι ι A<GOAL>Algebra.discr A (P.map ⇑(algebraMap A B) *ᵥ b) = P.det ^ 2 * Algebra.discr A b
<VAR>ι : Type w<VAR>DecidableEq ι<VAR>Fintype ι<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Module.Finite K L<VAR>Algebra.IsSeparable K L<VAR>b : Basis ι K L<GOAL>Algebra.discr K ⇑b ≠ 0
<VAR>ι : Type w<VAR>DecidableEq ι<VAR>Fintype ι<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Module.Finite K L<VAR>Algebra.IsSeparable K L<VAR>b : Basis ι K L<GOAL>IsUnit (Algebra.discr K ⇑b)
<VAR>ι : Type w<VAR>DecidableEq ι<VAR>Fintype ι<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>Field K<VAR>Field L<VAR>Field E<VAR>Algebra K L<VAR>Algebra K E<VAR>Module.Finite K L<VAR>IsAlgClosed E<VAR>b : ι → L<VAR>Algebra.IsSeparable K L<VAR>e : ι ≃ (L →ₐ[K] E)<GOAL>(algebraMap K E) (Algebra.discr K b) = (Algebra.embeddingsMatrixReindex K E b e).det ^ 2
<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>Field K<VAR>Field L<VAR>Field E<VAR>Algebra K L<VAR>Algebra K E<VAR>Module.Finite K L<VAR>IsAlgClosed E<VAR>pb : PowerBasis K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<VAR>Algebra.IsSeparable K L<GOAL>(algebraMap K E) (Algebra.discr K ⇑pb.basis) = ∏ i : Fin pb.dim, ∏ j ∈ Finset.Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2
<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>Field K<VAR>Field L<VAR>Field E<VAR>Algebra K L<VAR>Algebra K E<VAR>Module.Finite K L<VAR>IsAlgClosed E<VAR>pb : PowerBasis K L<VAR>Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>(algebraMap K E) (Algebra.discr K ⇑pb.basis) = ∏ i : Fin pb.dim, ∏ j ∈ Finset.Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))
<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>Field K<VAR>Field L<VAR>Field E<VAR>Algebra K L<VAR>Algebra K E<VAR>Module.Finite K L<VAR>IsAlgClosed E<VAR>pb : PowerBasis K L<VAR>Algebra.IsSeparable K L<VAR>e : Fin pb.dim ≃ (L →ₐ[K] E)<GOAL>(algebraMap K E) (Algebra.discr K ⇑pb.basis) = (-1) ^ (FiniteDimensional.finrank K L * (FiniteDimensional.finrank K L - 1) / 2) * ∏ i : Fin pb.dim, ∏ j ∈ Finset.Ioi i, ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)
<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Module.Finite K L<VAR>pb : PowerBasis K L<VAR>Algebra.IsSeparable K L<GOAL>Algebra.discr K ⇑pb.basis = (-1) ^ (FiniteDimensional.finrank K L * (FiniteDimensional.finrank K L - 1) / 2) * (Algebra.norm K) ((Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen)))
<VAR>ι : Type w<VAR>DecidableEq ι<VAR>Fintype ι<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Module.Finite K L<VAR>R : Type z<VAR>CommRing R<VAR>Algebra R K<VAR>Algebra R L<VAR>IsScalarTower R K L<VAR>b : ι → L<VAR>h : ∀ (i : ι), IsIntegral R (b i)<GOAL>IsIntegral R (Algebra.discr K b)
<VAR>K : Type u<VAR>L : Type v<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Module.Finite K L<VAR>R : Type z<VAR>CommRing R<VAR>Algebra R K<VAR>Algebra R L<VAR>IsScalarTower R K L<VAR>Algebra.IsSeparable K L<VAR>IsIntegrallyClosed R<VAR>IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<GOAL>Algebra.discr K ⇑B.basis • z ∈ Algebra.adjoin R {B.gen}
<VAR>A : Type u<VAR>ι : Type w<VAR>DecidableEq ι<VAR>CommRing A<VAR>Fintype ι<VAR>b b' : Basis ι ℤ A<GOAL>Algebra.discr ℤ ⇑b = Algebra.discr ℤ ⇑b'
<VAR>F : Type u_2<VAR>K : Type u_3<VAR>L : Type u_4<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F K<VAR>Algebra F L<VAR>s : Finset K<GOAL>(∀ x ∈ s, IsIntegral F x ∧ Polynomial.Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥(Algebra.adjoin F ↑s) →ₐ[F] L)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra R K<VAR>Algebra R L<VAR>x : L<VAR>int : IsIntegral R x<VAR>h : Polynomial.Splits (algebraMap R K) (minpoly R x)<VAR>f : K →ₐ[R] L<GOAL>x ∈ f.range
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>Algebra R K<VAR>Algebra R L<VAR>x : L<VAR>int : IsIntegral R x<VAR>h : Polynomial.Splits (algebraMap R K) (minpoly R x)<VAR>Algebra K L<VAR>IsScalarTower R K L<GOAL>x ∈ (algebraMap K L).range
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>CommRing M<VAR>Algebra R K<VAR>Algebra R M<VAR>Algebra K M<VAR>IsScalarTower R K M<VAR>x : M<VAR>int : IsIntegral R x<VAR>f : K →+* L<VAR>h : Polynomial.Splits (f.comp (algebraMap R K)) (minpoly R x)<GOAL>Polynomial.Splits f (minpoly K x)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>CommRing R<VAR>Field K<VAR>Field L<VAR>CommRing M<VAR>Algebra R K<VAR>Algebra R L<VAR>Algebra R M<VAR>Algebra K M<VAR>IsScalarTower R K M<VAR>x : M<VAR>int : IsIntegral R x<VAR>Algebra K L<VAR>IsScalarTower R K L<VAR>h : Polynomial.Splits (algebraMap R L) (minpoly R x)<GOAL>Polynomial.Splits (algebraMap K L) (minpoly K x)
<VAR>F : Type u_5<VAR>E : Type u_6<VAR>K : Type u_7<VAR>CommRing F<VAR>StrongRankCondition F<VAR>CommRing E<VAR>StrongRankCondition E<VAR>Ring K<VAR>SMul F E<VAR>Algebra E K<VAR>Algebra F K<VAR>IsScalarTower F E K<VAR>L : Subalgebra F K<VAR>Module.Free F ↥L<GOAL>Module.rank E ↥(Algebra.adjoin E ↑L) ≤ Module.rank F ↥L
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>CommSemiring A<VAR>Algebra R A<VAR>s t : Set A<VAR>h1 : (Subalgebra.toSubmodule (Algebra.adjoin R s)).FG<VAR>h2 : (Subalgebra.toSubmodule (Algebra.adjoin (↥(Algebra.adjoin R s)) t)).FG<GOAL>(Subalgebra.toSubmodule (Algebra.adjoin R (s ∪ t))).FG
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>s : Finset A<GOAL>(Algebra.adjoin R ↑s).FG
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>S.FG ↔ ∃ t, t.Finite ∧ Algebra.adjoin R t = S
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<GOAL>⊥.FG
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>(Subalgebra.toSubmodule S).FG → S.FG
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>IsNoetherian R A<VAR>S : Subalgebra R A<GOAL>S.FG
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>h : ⊤.FG<GOAL>⊤.FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>S : Subalgebra R A<VAR>T : Subalgebra R B<VAR>hS : S.FG<VAR>hT : T.FG<GOAL>(S.prod T).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<VAR>hs : S.FG<GOAL>(Subalgebra.map f S).FG
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>S : Subalgebra R A<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>hs : (Subalgebra.map f S).FG<GOAL>S.FG
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>S : Subalgebra R A<GOAL>⊤.FG ↔ S.FG
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>IsNoetherian R A<VAR>P : Subalgebra R A → Prop<VAR>base : P ⊥<VAR>ih : ∀ (S : Subalgebra R A) (x : A), P S → P (Algebra.adjoin R (insert x ↑S))<VAR>S : Subalgebra R A<GOAL>P S
<VAR>R : Type u<VAR>A : Type v<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>HS : S.FG<VAR>IsNoetherianRing R<GOAL>IsNoetherianRing ↥S
<VAR>R : Type u<VAR>CommRing R<VAR>s : Set R<VAR>hs : s.Finite<GOAL>IsNoetherianRing ↥(Subring.closure s)
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>self : IsDedekindDomainDvr A<GOAL>IsNoetherianRing A
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>self : IsDedekindDomainDvr A<VAR>P : Ideal A<GOAL>P ≠ ⊥ → ∀ (x : P.IsPrime), DiscreteValuationRing (Localization.AtPrime P)
<VAR>R : Type u_4<VAR>Rₘ : Type u_5<VAR>CommRing R<VAR>IsDomain R<VAR>CommRing Rₘ<VAR>Algebra R Rₘ<VAR>M : Submonoid R<VAR>IsLocalization M Rₘ<VAR>hM : M ≤ R⁰<VAR>h : Ring.DimensionLEOne R<GOAL>Ring.DimensionLEOne Rₘ
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>IsDedekindDomain A<VAR>M : Submonoid A<VAR>hM : M ≤ A⁰<VAR>Aₘ : Type u_4<VAR>CommRing Aₘ<VAR>IsDomain Aₘ<VAR>Algebra A Aₘ<VAR>IsLocalization M Aₘ<GOAL>IsDedekindDomain Aₘ
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>IsDedekindDomain A<VAR>P : Ideal A<VAR>P.IsPrime<VAR>Aₘ : Type u_4<VAR>CommRing Aₘ<VAR>IsDomain Aₘ<VAR>Algebra A Aₘ<VAR>IsLocalization.AtPrime Aₘ P<GOAL>IsDedekindDomain Aₘ
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<VAR>pP : P.IsPrime<VAR>Aₘ : Type u_4<VAR>CommRing Aₘ<VAR>Algebra A Aₘ<VAR>IsLocalization.AtPrime Aₘ P<GOAL>¬IsField Aₘ
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>IsDedekindDomain A<VAR>P : Ideal A<VAR>hP : P ≠ ⊥<VAR>pP : P.IsPrime<VAR>Aₘ : Type u_4<VAR>CommRing Aₘ<VAR>IsDomain Aₘ<VAR>Algebra A Aₘ<VAR>IsLocalization.AtPrime Aₘ P<GOAL>DiscreteValuationRing Aₘ
<VAR>A : Type u_2<VAR>CommRing A<VAR>IsDomain A<VAR>IsDedekindDomain A<GOAL>IsDedekindDomainDvr A
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>AddCommMonoid N<VAR>Module R N<VAR>p : MvPolynomial σ S<VAR>n : N<GOAL>MvPolynomial.rTensor (p ⊗ₜ[R] n) = Finsupp.sum p fun i m => Finsupp.single i (m ⊗ₜ[R] n)
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>AddCommMonoid N<VAR>Module R N<VAR>p : MvPolynomial σ S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(MvPolynomial.rTensor (p ⊗ₜ[R] n)) d = MvPolynomial.coeff d p ⊗ₜ[R] n
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>AddCommMonoid N<VAR>Module R N<VAR>e : σ →₀ ℕ<VAR>s : S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(MvPolynomial.rTensor ((MvPolynomial.monomial e) s ⊗ₜ[R] n)) d = if e = d then s ⊗ₜ[R] n else 0
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>AddCommMonoid N<VAR>Module R N<VAR>s : σ<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(MvPolynomial.rTensor (MvPolynomial.X s ⊗ₜ[R] n)) d = if Finsupp.single s 1 = d then 1 ⊗ₜ[R] n else 0
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>AddCommMonoid N<VAR>Module R N<VAR>t : TensorProduct R (MvPolynomial σ S) N<VAR>d : σ →₀ ℕ<GOAL>(MvPolynomial.rTensor t) d = (LinearMap.rTensor N (↑R (MvPolynomial.lcoeff S d))) t
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>AddCommMonoid N<VAR>Module R N<VAR>d : σ →₀ ℕ<VAR>s : S<VAR>n : N<GOAL>MvPolynomial.rTensor.symm (Finsupp.single d (s ⊗ₜ[R] n)) = (MvPolynomial.monomial d) s ⊗ₜ[R] n
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>AddCommMonoid N<VAR>Module R N<VAR>p : MvPolynomial σ R<VAR>n : N<GOAL>MvPolynomial.scalarRTensor (p ⊗ₜ[R] n) = Finsupp.sum p fun i m => Finsupp.single i (m • n)
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>AddCommMonoid N<VAR>Module R N<VAR>p : MvPolynomial σ R<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(MvPolynomial.scalarRTensor (p ⊗ₜ[R] n)) d = MvPolynomial.coeff d p • n
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>AddCommMonoid N<VAR>Module R N<VAR>e : σ →₀ ℕ<VAR>r : R<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(MvPolynomial.scalarRTensor ((MvPolynomial.monomial e) r ⊗ₜ[R] n)) d = if e = d then r • n else 0
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>AddCommMonoid N<VAR>Module R N<VAR>s : σ<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>(MvPolynomial.scalarRTensor (MvPolynomial.X s ⊗ₜ[R] n)) d = if Finsupp.single s 1 = d then n else 0
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>AddCommMonoid N<VAR>Module R N<VAR>d : σ →₀ ℕ<VAR>n : N<GOAL>MvPolynomial.scalarRTensor.symm (Finsupp.single d n) = (MvPolynomial.monomial d) 1 ⊗ₜ[R] n
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>CommSemiring N<VAR>Algebra R N<VAR>p : MvPolynomial σ S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>MvPolynomial.coeff d (MvPolynomial.rTensorAlgHom (p ⊗ₜ[R] n)) = MvPolynomial.coeff d p ⊗ₜ[R] n
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>CommSemiring N<VAR>Algebra R N<VAR>e : σ →₀ ℕ<VAR>s : S<VAR>n : N<VAR>d : σ →₀ ℕ<GOAL>MvPolynomial.coeff d (MvPolynomial.rTensorAlgHom ((MvPolynomial.monomial e) s ⊗ₜ[R] n)) = if e = d then s ⊗ₜ[R] n else 0
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>CommSemiring N<VAR>Algebra R N<GOAL>MvPolynomial.rTensorAlgHom.toLinearMap = ↑MvPolynomial.rTensor
<VAR>R : Type u<VAR>N : Type w<VAR>CommSemiring R<VAR>σ : Type u_1<VAR>DecidableEq σ<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>CommSemiring N<VAR>Algebra R N<VAR>p : TensorProduct R (MvPolynomial σ S) N<GOAL>MvPolynomial.rTensorAlgHom p = MvPolynomial.rTensor p