ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<VAR>he : ∀ (i : I), IsIdempotentElem (e i)<VAR>he₁ : ∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0<VAR>he₂ : ∏ i : I, e i = 0<GOAL>Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e i}))
<VAR>R : Type u<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>Rₚ : Type v<VAR>CommSemiring Rₚ<VAR>Algebra R Rₚ<VAR>IsLocalization S Rₚ<VAR>M : Type w<VAR>AddCommMonoid M<VAR>Module R M<VAR>Mₚ : Type t<VAR>AddCommMonoid Mₚ<VAR>Module R Mₚ<VAR>Module Rₚ Mₚ<VAR>IsScalarTower R Rₚ Mₚ<VAR>f : M →ₗ[R] Mₚ<VAR>IsLocalizedModule S f<VAR>Module.Finite R M<GOAL>Module.Finite Rₚ Mₚ
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type w<VAR>AddCommMonoid M<VAR>Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>Mₚ : { x // x ∈ t } → Type u_1<VAR>(g : { x // x ∈ t }) → AddCommMonoid (Mₚ g)<VAR>(g : { x // x ∈ t }) → Module R (Mₚ g)<VAR>Rₚ : { x // x ∈ t } → Type u<VAR>(g : { x // x ∈ t }) → CommRing (Rₚ g)<VAR>(g : { x // x ∈ t }) → Algebra R (Rₚ g)<VAR>∀ (g : { x // x ∈ t }), IsLocalization.Away (↑g) (Rₚ g)<VAR>(g : { x // x ∈ t }) → Module (Rₚ g) (Mₚ g)<VAR>∀ (g : { x // x ∈ t }), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : { x // x ∈ t }) → M →ₗ[R] Mₚ g<VAR>∀ (g : { x // x ∈ t }), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : { x // x ∈ t }), Module.Finite (Rₚ g) (Mₚ g)<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type w<VAR>AddCommMonoid M<VAR>Module R M<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>Mₚ : ↑t → Type u_1<VAR>(g : ↑t) → AddCommMonoid (Mₚ g)<VAR>(g : ↑t) → Module R (Mₚ g)<VAR>Rₚ : ↑t → Type u<VAR>(g : ↑t) → CommRing (Rₚ g)<VAR>(g : ↑t) → Algebra R (Rₚ g)<VAR>h₁ : ∀ (g : ↑t), IsLocalization.Away (↑g) (Rₚ g)<VAR>(g : ↑t) → Module (Rₚ g) (Mₚ g)<VAR>∀ (g : ↑t), IsScalarTower R (Rₚ g) (Mₚ g)<VAR>f : (g : ↑t) → M →ₗ[R] Mₚ g<VAR>h₂ : ∀ (g : ↑t), IsLocalizedModule (Submonoid.powers ↑g) (f g)<VAR>H : ∀ (g : ↑t), Module.Finite (Rₚ g) (Mₚ g)<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type w<VAR>AddCommMonoid M<VAR>Module R M<VAR>t : Finset R<VAR>ht : Ideal.span ↑t = ⊤<VAR>H : ∀ (g : { x // x ∈ t }), Module.Finite (Localization.Away ↑g) (LocalizedModule (Submonoid.powers ↑g) M)<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>CommRing R<VAR>M : Type w<VAR>AddCommMonoid M<VAR>Module R M<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>H : ∀ (g : ↑t), Module.Finite (Localization.Away ↑g) (LocalizedModule (Submonoid.powers ↑g) M)<GOAL>Module.Finite R M
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>H : ∀ (g : ↑t), (Ideal.map (algebraMap R (Localization.Away ↑g)) I).FG<GOAL>I.FG
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>CommRing S<VAR>f : R →+* S<VAR>t : Set R<VAR>ht : Ideal.span t = ⊤<VAR>H : ∀ (g : ↑t), (RingHom.ker (Localization.awayMap f ↑g)).FG<GOAL>(RingHom.ker f).FG
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>LocalRing R<GOAL>∃! I, I.IsMaximal
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>LocalRing R<VAR>I : Ideal R<VAR>hI : I.IsMaximal<GOAL>I = LocalRing.maximalIdeal R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>LocalRing R<VAR>J : Ideal R<VAR>hJ : J ≠ ⊤<GOAL>J ≤ LocalRing.maximalIdeal R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>LocalRing R<VAR>x : R<GOAL>x ∈ LocalRing.maximalIdeal R ↔ x ∈ nonunits R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>LocalRing R<GOAL>IsField R ↔ LocalRing.maximalIdeal R = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>I : Ideal R<GOAL>LocalRing.maximalIdeal R ≤ I.jacobson
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>I : Ideal R<VAR>h : I ≠ ⊤<GOAL>I.jacobson = LocalRing.maximalIdeal R
<VAR>R : Type u_1<VAR>K : Type u_3<VAR>CommRing R<VAR>LocalRing R<VAR>Field K<VAR>φ : R →+* K<VAR>hφ : Function.Surjective ⇑φ<GOAL>RingHom.ker φ = LocalRing.maximalIdeal R
<VAR>R : Type u_4<VAR>Field R<GOAL>LocalRing.maximalIdeal R = ⊥
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring P<VAR>CommSemiring Q<VAR>M : Submonoid R<VAR>T : Submonoid P<VAR>Algebra R S<VAR>Algebra P Q<VAR>IsLocalization M S<VAR>IsLocalization T Q<VAR>g : R →+* P<VAR>hT : Submonoid.map g M = T<GOAL>RingHom.ker (IsLocalization.map Q g ⋯) = Ideal.map (algebraMap R S) (RingHom.ker g)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring P<VAR>CommSemiring Q<VAR>M : Submonoid R<VAR>T : Submonoid P<VAR>Algebra R S<VAR>Algebra P Q<VAR>IsLocalization M S<VAR>IsLocalization T Q<VAR>g : R →+* P<VAR>hy : M ≤ Submonoid.comap g T<VAR>r : ↥(RingHom.ker g)<GOAL>↑((RingHom.toKerIsLocalization S Q g hy) r) = (algebraMap R S) ↑r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>CommSemiring R<VAR>CommSemiring S<VAR>CommSemiring P<VAR>CommSemiring Q<VAR>M : Submonoid R<VAR>T : Submonoid P<VAR>Algebra R S<VAR>Algebra P Q<VAR>IsLocalization M S<VAR>IsLocalization T Q<VAR>g : R →+* P<VAR>hT : Submonoid.map g M = T<GOAL>IsLocalizedModule M (RingHom.toKerIsLocalization S Q g ⋯)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Submonoid R<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>Rₚ : Type u'<VAR>CommRing Rₚ<VAR>Algebra R Rₚ<VAR>IsLocalization M Rₚ<VAR>Aₚ : Type v'<VAR>CommRing Aₚ<VAR>Algebra R Aₚ<VAR>Algebra A Aₚ<VAR>IsScalarTower R A Aₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ<VAR>Bₚ : Type v'<VAR>CommRing Bₚ<VAR>Algebra R Bₚ<VAR>Algebra B Bₚ<VAR>IsScalarTower R B Bₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ<VAR>Algebra Rₚ Aₚ<VAR>Algebra Rₚ Bₚ<VAR>IsScalarTower R Rₚ Aₚ<VAR>IsScalarTower R Rₚ Bₚ<VAR>f : A →ₐ[R] B<GOAL>⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f) = ⇑(IsLocalization.map Bₚ f.toRingHom ⋯)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Submonoid R<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>Rₚ : Type u'<VAR>CommRing Rₚ<VAR>Algebra R Rₚ<VAR>IsLocalization M Rₚ<VAR>Aₚ : Type v'<VAR>CommRing Aₚ<VAR>Algebra R Aₚ<VAR>Algebra A Aₚ<VAR>IsScalarTower R A Aₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ<VAR>Bₚ : Type v'<VAR>CommRing Bₚ<VAR>Algebra R Bₚ<VAR>Algebra B Bₚ<VAR>IsScalarTower R B Bₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ<VAR>Algebra Rₚ Aₚ<VAR>Algebra Rₚ Bₚ<VAR>IsScalarTower R Rₚ Aₚ<VAR>IsScalarTower R Rₚ Bₚ<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Submonoid R<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>Rₚ : Type u'<VAR>CommRing Rₚ<VAR>Algebra R Rₚ<VAR>IsLocalization M Rₚ<VAR>Aₚ : Type v'<VAR>CommRing Aₚ<VAR>Algebra R Aₚ<VAR>Algebra A Aₚ<VAR>IsScalarTower R A Aₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ<VAR>Bₚ : Type v'<VAR>CommRing Bₚ<VAR>Algebra R Bₚ<VAR>Algebra B Bₚ<VAR>IsScalarTower R B Bₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ<VAR>Algebra Rₚ Aₚ<VAR>Algebra Rₚ Bₚ<VAR>IsScalarTower R Rₚ Aₚ<VAR>IsScalarTower R Rₚ Bₚ<VAR>f : A →ₐ[R] B<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(IsLocalization.mapₐ M Rₚ Aₚ Bₚ f)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Submonoid R<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>Rₚ : Type u'<VAR>CommRing Rₚ<VAR>Algebra R Rₚ<VAR>IsLocalization M Rₚ<VAR>Aₚ : Type v'<VAR>CommRing Aₚ<VAR>Algebra R Aₚ<VAR>Algebra A Aₚ<VAR>IsScalarTower R A Aₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ<VAR>Bₚ : Type v'<VAR>CommRing Bₚ<VAR>Algebra R Bₚ<VAR>Algebra B Bₚ<VAR>IsScalarTower R B Bₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ<VAR>Algebra Rₚ Aₚ<VAR>Algebra Rₚ Bₚ<VAR>IsScalarTower R Rₚ Aₚ<VAR>IsScalarTower R Rₚ Bₚ<VAR>f : A →ₐ[R] B<VAR>x : ↥(RingHom.ker f)<GOAL>(AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f) x = (RingHom.toKerIsLocalization Aₚ Bₚ f.toRingHom ⋯) x
<VAR>R : Type u<VAR>CommRing R<VAR>M : Submonoid R<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type w<VAR>CommRing B<VAR>Algebra R B<VAR>Rₚ : Type u'<VAR>CommRing Rₚ<VAR>Algebra R Rₚ<VAR>IsLocalization M Rₚ<VAR>Aₚ : Type v'<VAR>CommRing Aₚ<VAR>Algebra R Aₚ<VAR>Algebra A Aₚ<VAR>IsScalarTower R A Aₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid A M) Aₚ<VAR>Bₚ : Type v'<VAR>CommRing Bₚ<VAR>Algebra R Bₚ<VAR>Algebra B Bₚ<VAR>IsScalarTower R B Bₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid B M) Bₚ<VAR>Algebra Rₚ Aₚ<VAR>Algebra Rₚ Bₚ<VAR>IsScalarTower R Rₚ Aₚ<VAR>IsScalarTower R Rₚ Bₚ<VAR>f : A →ₐ[R] B<GOAL>IsLocalizedModule (Algebra.algebraMapSubmonoid A M) (AlgHom.toKerIsLocalization M Rₚ Aₚ Bₚ f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>h : PowerBasis R S<GOAL>(BilinForm.toMatrix h.basis) (Algebra.traceForm R S) = Matrix.of fun i j => (Algebra.trace R S) (h.gen ^ (↑i + ↑j))
<VAR>S : Type u_2<VAR>CommRing S<VAR>K : Type u_4<VAR>Field K<VAR>Algebra K S<VAR>Nontrivial S<VAR>pb : PowerBasis K S<GOAL>(Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff
<VAR>S : Type u_2<VAR>CommRing S<VAR>K : Type u_4<VAR>Field K<VAR>F : Type u_6<VAR>Field F<VAR>Algebra K S<VAR>Algebra K F<VAR>Nontrivial S<VAR>pb : PowerBasis K S<VAR>hf : Polynomial.Splits (algebraMap K F) (minpoly K pb.gen)<GOAL>(algebraMap K F) ((Algebra.trace K S) pb.gen) = ((minpoly K pb.gen).aroots F).sum
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>hx : ¬IsIntegral K x<GOAL>(Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x) = 0
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : Type u_6<VAR>Field F<VAR>Algebra K F<VAR>x : L<VAR>hf : Polynomial.Splits (algebraMap K F) (minpoly K x)<GOAL>(algebraMap K F) ((Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).sum
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>x : L<GOAL>(Algebra.trace K L) x = FiniteDimensional.finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (IntermediateField.AdjoinSimple.gen K x)
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : Type u_6<VAR>Field F<VAR>Algebra K F<VAR>FiniteDimensional K L<VAR>x : L<VAR>hF : Polynomial.Splits (algebraMap K F) (minpoly K x)<GOAL>(algebraMap K F) ((Algebra.trace K L) x) = FiniteDimensional.finrank (↥K⟮x⟯) L • ((minpoly K x).aroots F).sum
<VAR>R : Type u_1<VAR>CommRing R<VAR>L : Type u_5<VAR>Field L<VAR>F : Type u_6<VAR>Field F<VAR>Algebra R L<VAR>Algebra L F<VAR>Algebra R F<VAR>IsScalarTower R L F<VAR>FiniteDimensional L F<VAR>x : F<VAR>hx : IsIntegral R x<GOAL>IsIntegral R ((Algebra.trace L F) x)
<VAR>A : Type u_7<VAR>B : Type u_8<VAR>C : Type u_9<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra A B<VAR>Algebra A C<VAR>e : B ≃ₐ[A] C<VAR>x : B<GOAL>(Algebra.trace A C) (e x) = (Algebra.trace A B) x
<VAR>A : Type u_7<VAR>B : Type u_8<VAR>C : Type u_9<VAR>CommRing A<VAR>CommRing B<VAR>CommRing C<VAR>Algebra A C<VAR>Algebra B C<VAR>e : A ≃+* B<VAR>he : (algebraMap B C).comp ↑e = algebraMap A C<VAR>x : C<GOAL>e ((Algebra.trace A C) x) = (Algebra.trace B C) x
<VAR>A₁ : Type u_7<VAR>B₁ : Type u_8<VAR>A₂ : Type u_9<VAR>B₂ : Type u_10<VAR>CommRing A₁<VAR>CommRing B₁<VAR>CommRing A₂<VAR>CommRing B₂<VAR>Algebra A₁ B₁<VAR>Algebra A₂ B₂<VAR>e₁ : A₁ ≃+* A₂<VAR>e₂ : B₁ ≃+* B₂<VAR>he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)<VAR>x : B₁<GOAL>(Algebra.trace A₁ B₁) x = e₁.symm ((Algebra.trace A₂ B₂) (e₂ x))
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E : Type u_7<VAR>Field E<VAR>Algebra K E<VAR>pb : PowerBasis K L<VAR>hE : Polynomial.Splits (algebraMap K E) (minpoly K pb.gen)<VAR>hfx : IsSeparable K pb.gen<GOAL>(algebraMap K E) ((Algebra.trace K L) pb.gen) = ∑ σ : L →ₐ[K] E, σ pb.gen
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>F : Type u_6<VAR>Field F<VAR>Algebra L F<VAR>Algebra K F<VAR>IsScalarTower K L F<VAR>E : Type u_7<VAR>Field E<VAR>Algebra K E<VAR>IsAlgClosed E<VAR>FiniteDimensional K F<VAR>Algebra.IsSeparable K F<VAR>pb : PowerBasis K L<GOAL>∑ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = FiniteDimensional.finrank L F • ∑ σ : L →ₐ[K] E, σ pb.gen
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>E : Type u_7<VAR>Field E<VAR>Algebra K E<VAR>IsAlgClosed E<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>x : L<GOAL>(algebraMap K E) ((Algebra.trace K L) x) = ∑ σ : L →ₐ[K] E, σ x
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>x : L<VAR>FiniteDimensional K L<VAR>IsGalois K L<GOAL>(algebraMap K L) ((Algebra.trace K L) x) = ∑ σ : L ≃ₐ[K] L, σ x
<VAR>κ : Type w<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>b : κ → B<VAR>i j : κ<GOAL>Algebra.traceMatrix A b i j = ((Algebra.traceForm A B) (b i)) (b j)
<VAR>κ : Type w<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>κ' : Type u_7<VAR>b : Basis κ A B<VAR>f : κ ≃ κ'<GOAL>Algebra.traceMatrix A ⇑(b.reindex f) = (Matrix.reindex f f) (Algebra.traceMatrix A ⇑b)
<VAR>κ : Type w<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<GOAL>Algebra.traceMatrix A (b ᵥ* P.map ⇑(algebraMap A B)) = Pᵀ * Algebra.traceMatrix A b * P
<VAR>κ : Type w<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Fintype κ<VAR>b : κ → B<VAR>P : Matrix κ κ A<GOAL>Algebra.traceMatrix A (P.map ⇑(algebraMap A B) *ᵥ b) = P * Algebra.traceMatrix A b * Pᵀ
<VAR>κ : Type w<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Fintype κ<VAR>DecidableEq κ<VAR>b : Basis κ A B<GOAL>Algebra.traceMatrix A ⇑b = (BilinForm.toMatrix b) (Algebra.traceForm A B)
<VAR>ι : Type w<VAR>Fintype ι<VAR>A : Type u<VAR>B : Type v<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>b : Basis ι A B<VAR>z : B<GOAL>Algebra.traceMatrix A ⇑b *ᵥ b.equivFun z = fun i => (Algebra.trace A B) (z * b i)
<VAR>κ : Type w<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>CommRing C<VAR>Algebra A C<VAR>b : κ → B<VAR>i : κ<VAR>σ : B →ₐ[A] C<GOAL>Algebra.embeddingsMatrix A C b i σ = σ (b i)
<VAR>A : Type u<VAR>B : Type v<VAR>C : Type z<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>CommRing C<VAR>Algebra A C<VAR>pb : PowerBasis A B<VAR>e : Fin pb.dim ≃ (B →ₐ[A] C)<GOAL>Algebra.embeddingsMatrixReindex A C (⇑pb.basis) e = (Matrix.vandermonde fun i => (e i) pb.gen)ᵀ
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>κ : Type w<VAR>E : Type z<VAR>Field E<VAR>Algebra K E<VAR>Module.Finite K L<VAR>Algebra.IsSeparable K L<VAR>IsAlgClosed E<VAR>b : κ → L<GOAL>(Algebra.traceMatrix K b).map ⇑(algebraMap K E) = Algebra.embeddingsMatrix K E b * (Algebra.embeddingsMatrix K E b)ᵀ
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>κ : Type w<VAR>E : Type z<VAR>Field E<VAR>Algebra K E<VAR>Module.Finite K L<VAR>Algebra.IsSeparable K L<VAR>IsAlgClosed E<VAR>b : κ → L<VAR>Fintype κ<VAR>e : κ ≃ (L →ₐ[K] E)<GOAL>(Algebra.traceMatrix K b).map ⇑(algebraMap K E) = Algebra.embeddingsMatrixReindex K E b e * (Algebra.embeddingsMatrixReindex K E b e)ᵀ
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>pb : PowerBasis K L<VAR>Algebra.IsSeparable K L<GOAL>(Algebra.traceMatrix K ⇑pb.basis).det ≠ 0
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>ι : Type w<VAR>Fintype ι<VAR>Algebra.IsSeparable K L<VAR>DecidableEq ι<VAR>b : Basis ι K L<GOAL>((BilinForm.toMatrix b) (Algebra.traceForm K L)).det ≠ 0
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<GOAL>(Algebra.traceForm K L).Nondegenerate
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<GOAL>Algebra.trace K L ≠ 0
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<GOAL>Function.Surjective ⇑(Algebra.trace K L)
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>pb : PowerBasis K L<VAR>i : Fin pb.dim<GOAL>((Algebra.traceForm K L).dualBasis ⋯ pb.basis) i = (minpolyDiv K pb.gen).coeff ↑i / (Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen))
<VAR>R : Type u<VAR>CommRing R<VAR>σ : Type u_1<GOAL>(↑(KaehlerDifferential.mvPolynomialBasis R σ).repr).compDer (KaehlerDifferential.D R (MvPolynomial σ R)) = MvPolynomial.mkDerivation R fun x => Finsupp.single x 1
<VAR>R : Type u<VAR>CommRing R<VAR>σ : Type u_1<VAR>x : MvPolynomial σ R<GOAL>(KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x) = (MvPolynomial.mkDerivation R fun x => Finsupp.single x 1) x
<VAR>R : Type u<VAR>CommRing R<VAR>σ : Type u_1<VAR>i : σ<GOAL>(KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)) = Finsupp.single i 1
<VAR>R : Type u<VAR>CommRing R<VAR>σ : Type u_1<VAR>x : MvPolynomial σ R<VAR>i : σ<GOAL>((KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x)) i = (MvPolynomial.pderiv i) x
<VAR>R : Type u<VAR>CommRing R<VAR>σ : Type u_1<VAR>i : σ<VAR>x : MvPolynomial σ R<GOAL>(KaehlerDifferential.mvPolynomialBasis R σ).repr.symm (Finsupp.single i x) = x • (KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)
<VAR>R : Type u<VAR>CommRing R<VAR>σ : Type u_1<VAR>i : σ<GOAL>(KaehlerDifferential.mvPolynomialBasis R σ) i = (KaehlerDifferential.D R (MvPolynomial σ R)) (MvPolynomial.X i)
<VAR>R : Type u<VAR>CommRing R<VAR>P : Polynomial R<GOAL>(KaehlerDifferential.D R (Polynomial R)) P = Polynomial.derivative P • (KaehlerDifferential.D R (Polynomial R)) Polynomial.X
<VAR>R : Type u<VAR>CommRing R<GOAL>(KaehlerDifferential.polynomialEquiv R).compDer (KaehlerDifferential.D R (Polynomial R)) = Polynomial.derivative'
<VAR>R : Type u<VAR>CommRing R<VAR>P : Polynomial R<GOAL>(KaehlerDifferential.polynomialEquiv R) ((KaehlerDifferential.D R (Polynomial R)) P) = Polynomial.derivative P
<VAR>R : Type u<VAR>CommRing R<VAR>P : Polynomial R<GOAL>(KaehlerDifferential.polynomialEquiv R).symm P = P • (KaehlerDifferential.D R (Polynomial R)) Polynomial.X
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<GOAL>RingHom.ker (LocalRing.residue R) = LocalRing.maximalIdeal R
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>x : R<GOAL>(LocalRing.residue R) x = 0 ↔ x ∈ LocalRing.maximalIdeal R
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>x : R<GOAL>(LocalRing.residue R) x ≠ 0 ↔ IsUnit x
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<GOAL>algebraMap R (LocalRing.ResidueField R) = LocalRing.residue R
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommRing R<VAR>LocalRing R<VAR>Field S<VAR>f : R →+* S<VAR>IsLocalRingHom f<GOAL>(LocalRing.ResidueField.lift f).comp (LocalRing.residue R) = f
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommRing R<VAR>LocalRing R<VAR>Field S<VAR>f : R →+* S<VAR>IsLocalRingHom f<VAR>x : R<GOAL>(LocalRing.ResidueField.lift f) ((LocalRing.residue R) x) = f x
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<GOAL>LocalRing.ResidueField.map (RingHom.id R) = RingHom.id (LocalRing.ResidueField R)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>LocalRing R<VAR>CommRing S<VAR>LocalRing S<VAR>CommRing T<VAR>LocalRing T<VAR>f : T →+* R<VAR>g : R →+* S<VAR>IsLocalRingHom f<VAR>IsLocalRingHom g<GOAL>LocalRing.ResidueField.map (g.comp f) = (LocalRing.ResidueField.map g).comp (LocalRing.ResidueField.map f)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>LocalRing R<VAR>CommRing S<VAR>LocalRing S<VAR>f : R →+* S<VAR>IsLocalRingHom f<GOAL>(LocalRing.ResidueField.map f).comp (LocalRing.residue R) = (LocalRing.residue S).comp f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>LocalRing R<VAR>CommRing S<VAR>LocalRing S<VAR>f : R →+* S<VAR>IsLocalRingHom f<VAR>r : R<GOAL>(LocalRing.ResidueField.map f) ((LocalRing.residue R) r) = (LocalRing.residue S) (f r)
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>x : LocalRing.ResidueField R<GOAL>(LocalRing.ResidueField.map (RingHom.id R)) x = x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>LocalRing R<VAR>CommRing S<VAR>LocalRing S<VAR>CommRing T<VAR>LocalRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>x : LocalRing.ResidueField R<VAR>IsLocalRingHom f<VAR>IsLocalRingHom g<GOAL>(LocalRing.ResidueField.map g) ((LocalRing.ResidueField.map f) x) = (LocalRing.ResidueField.map (g.comp f)) x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>LocalRing R<VAR>CommRing S<VAR>LocalRing S<VAR>f : R ≃+* S<VAR>a : LocalRing.ResidueField R<GOAL>(LocalRing.ResidueField.mapEquiv f) a = (LocalRing.ResidueField.map ↑f) a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>LocalRing R<VAR>CommRing S<VAR>LocalRing S<VAR>f : R ≃+* S<GOAL>(LocalRing.ResidueField.mapEquiv f).symm = LocalRing.ResidueField.mapEquiv f.symm
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>LocalRing R<VAR>CommRing S<VAR>LocalRing S<VAR>CommRing T<VAR>LocalRing T<VAR>e₁ : R ≃+* S<VAR>e₂ : S ≃+* T<GOAL>LocalRing.ResidueField.mapEquiv (e₁.trans e₂) = (LocalRing.ResidueField.mapEquiv e₁).trans (LocalRing.ResidueField.mapEquiv e₂)
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<GOAL>LocalRing.ResidueField.mapEquiv (RingEquiv.refl R) = RingEquiv.refl (LocalRing.ResidueField R)
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>f : R ≃+* R<GOAL>LocalRing.ResidueField.mapAut f = LocalRing.ResidueField.mapEquiv f
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>G : Type u_4<VAR>Group G<VAR>MulSemiringAction G R<VAR>g : G<VAR>r : R<GOAL>(LocalRing.residue R) (g • r) = g • (LocalRing.residue R) r
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<GOAL>IsLocalRingHom (LocalRing.residue R)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>self : I.Filtration M<VAR>i : ℕ<GOAL>self.N (i + 1) ≤ self.N i
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>AddCommGroup M<VAR>Module R M<VAR>self : I.Filtration M<VAR>i : ℕ<GOAL>I • self.N i ≤ self.N (i + 1)
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>i j : ℕ<GOAL>I ^ i • F.N j ≤ F.N (i + j)
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<VAR>i j k : ℕ<GOAL>I ^ (i + k) • F.N j ≤ I ^ k • F.N (i + j)
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F : I.Filtration M<GOAL>Antitone F.N
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<GOAL>∀ (x : ℕ), (I.trivialFiltration N).N x = N
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<GOAL>(F ⊔ F').N = F.N ⊔ F'.N
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>S : Set (I.Filtration M)<GOAL>(sSup S).N = sSup (Ideal.Filtration.N '' S)
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<GOAL>(F ⊓ F').N = F.N ⊓ F'.N
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>S : Set (I.Filtration M)<GOAL>(sInf S).N = sInf (Ideal.Filtration.N '' S)
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>⊤.N = ⊤
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<GOAL>⊥.N = ⊥
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>ι : Sort u_1<VAR>f : ι → I.Filtration M<GOAL>(iSup f).N = ⨆ i, (f i).N
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>ι : Sort u_1<VAR>f : ι → I.Filtration M<GOAL>(iInf f).N = ⨅ i, (f i).N
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>i : ℕ<GOAL>(I.stableFiltration N).N i = I ^ i • N
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<GOAL>(I.stableFiltration N).Stable