ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℕ<VAR>a : R<VAR>φ : PowerSeries R<GOAL>(PowerSeries.coeff R n) (PowerSeries.inv.aux a φ) = if n = 0 then a else -a * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (PowerSeries.coeff R x.1) φ * (PowerSeries.coeff R x.2) (PowerSeries.inv.aux a φ) else 0
<VAR>R : Type u_1<VAR>Ring R<VAR>n : ℕ<VAR>φ : PowerSeries R<VAR>u : Rˣ<GOAL>(PowerSeries.coeff R n) (φ.invOfUnit u) = if n = 0 then ↑u⁻¹ else -↑u⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (PowerSeries.coeff R x.1) φ * (PowerSeries.coeff R x.2) (φ.invOfUnit u) else 0
<VAR>R : Type u_1<VAR>Ring R<VAR>φ : PowerSeries R<VAR>u : Rˣ<GOAL>(PowerSeries.constantCoeff R) (φ.invOfUnit u) = ↑u⁻¹
<VAR>R : Type u_1<VAR>Ring R<VAR>φ : PowerSeries R<VAR>u : Rˣ<VAR>h : (PowerSeries.constantCoeff R) φ = ↑u<GOAL>φ * φ.invOfUnit u = 1
<VAR>R : Type u_1<VAR>Ring R<VAR>φ : PowerSeries R<VAR>u : Rˣ<VAR>h : (PowerSeries.constantCoeff R) φ = ↑u<GOAL>φ.invOfUnit u * φ = 1
<VAR>R : Type u_1<VAR>Ring R<VAR>φ : PowerSeries R<GOAL>IsUnit φ ↔ IsUnit ((PowerSeries.constantCoeff R) φ)
<VAR>R : Type u_1<VAR>Ring R<VAR>φ : PowerSeries R<GOAL>φ - (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ) = (PowerSeries.mk fun p => (PowerSeries.coeff R (p + 1)) φ) * PowerSeries.X
<VAR>R : Type u_1<VAR>Ring R<VAR>φ : PowerSeries R<GOAL>φ - (PowerSeries.C R) ((PowerSeries.constantCoeff R) φ) = PowerSeries.X * PowerSeries.mk fun p => (PowerSeries.coeff R (p + 1)) φ
<VAR>k : Type u_2<VAR>Field k<VAR>φ : PowerSeries k<GOAL>φ⁻¹ = PowerSeries.inv.aux ((PowerSeries.constantCoeff k) φ)⁻¹ φ
<VAR>k : Type u_2<VAR>Field k<VAR>n : ℕ<VAR>φ : PowerSeries k<GOAL>(PowerSeries.coeff k n) φ⁻¹ = if n = 0 then ((PowerSeries.constantCoeff k) φ)⁻¹ else -((PowerSeries.constantCoeff k) φ)⁻¹ * ∑ x ∈ Finset.antidiagonal n, if x.2 < n then (PowerSeries.coeff k x.1) φ * (PowerSeries.coeff k x.2) φ⁻¹ else 0
<VAR>k : Type u_2<VAR>Field k<VAR>φ : PowerSeries k<GOAL>(PowerSeries.constantCoeff k) φ⁻¹ = ((PowerSeries.constantCoeff k) φ)⁻¹
<VAR>k : Type u_2<VAR>Field k<VAR>φ : PowerSeries k<GOAL>φ⁻¹ = 0 ↔ (PowerSeries.constantCoeff k) φ = 0
<VAR>k : Type u_2<VAR>Field k<GOAL>0⁻¹ = 0
<VAR>k : Type u_2<VAR>Field k<VAR>φ : PowerSeries k<VAR>h : (PowerSeries.constantCoeff k) φ ≠ 0<GOAL>φ.invOfUnit (Units.mk0 ((PowerSeries.constantCoeff k) φ) h) = φ⁻¹
<VAR>k : Type u_2<VAR>Field k<VAR>φ : PowerSeries k<VAR>u : kˣ<VAR>h : (PowerSeries.constantCoeff k) φ = ↑u<GOAL>φ.invOfUnit u = φ⁻¹
<VAR>k : Type u_2<VAR>Field k<VAR>φ : PowerSeries k<VAR>h : (PowerSeries.constantCoeff k) φ ≠ 0<GOAL>φ * φ⁻¹ = 1
<VAR>k : Type u_2<VAR>Field k<VAR>φ : PowerSeries k<VAR>h : (PowerSeries.constantCoeff k) φ ≠ 0<GOAL>φ⁻¹ * φ = 1
<VAR>k : Type u_2<VAR>Field k<VAR>φ₁ φ₂ φ₃ : PowerSeries k<VAR>h : (PowerSeries.constantCoeff k) φ₃ ≠ 0<GOAL>φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂
<VAR>k : Type u_2<VAR>Field k<VAR>φ ψ : PowerSeries k<VAR>h : (PowerSeries.constantCoeff k) ψ ≠ 0<GOAL>φ = ψ⁻¹ ↔ φ * ψ = 1
<VAR>k : Type u_2<VAR>Field k<VAR>φ ψ : PowerSeries k<VAR>h : (PowerSeries.constantCoeff k) ψ ≠ 0<GOAL>ψ⁻¹ = φ ↔ φ * ψ = 1
<VAR>k : Type u_2<VAR>Field k<VAR>φ ψ : PowerSeries k<GOAL>(φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹
<VAR>k : Type u_2<VAR>Field k<VAR>r : k<GOAL>((PowerSeries.C k) r)⁻¹ = (PowerSeries.C k) r⁻¹
<VAR>k : Type u_2<VAR>Field k<GOAL>PowerSeries.X⁻¹ = 0
<VAR>k : Type u_2<VAR>Field k<VAR>r : k<VAR>φ : PowerSeries k<GOAL>(r • φ)⁻¹ = r⁻¹ • φ⁻¹
<VAR>k : Type u_2<VAR>Field k<VAR>f : PowerSeries k<VAR>hf : f ≠ 0<GOAL>PowerSeries.divided_by_X_pow_order hf * PowerSeries.Inv_divided_by_X_pow_order hf = 1
<VAR>k : Type u_2<VAR>Field k<VAR>f : PowerSeries k<VAR>hf : f ≠ 0<GOAL>PowerSeries.Inv_divided_by_X_pow_order hf * PowerSeries.divided_by_X_pow_order hf = 1
<VAR>k : Type u_2<VAR>Field k<VAR>f : PowerSeries k<VAR>hf : f ≠ 0<GOAL>IsUnit (PowerSeries.divided_by_X_pow_order hf)
<VAR>k : Type u_2<VAR>Field k<VAR>f : PowerSeries k<VAR>hf : f ≠ 0<GOAL>↑f.Unit_of_divided_by_X_pow_order = PowerSeries.divided_by_X_pow_order hf
<VAR>k : Type u_2<VAR>Field k<GOAL>PowerSeries.Unit_of_divided_by_X_pow_order 0 = 1
<VAR>k : Type u_2<VAR>Field k<VAR>f : PowerSeries k<VAR>hf : f ≠ 0<GOAL>f = PowerSeries.divided_by_X_pow_order hf ↔ IsUnit f
<VAR>k : Type u_2<VAR>Field k<GOAL>DiscreteValuationRing.HasUnitMulPowIrreducibleFactorization (PowerSeries k)
<VAR>k : Type u_2<VAR>Field k<GOAL>LocalRing.maximalIdeal (PowerSeries k) = Ideal.span {PowerSeries.X}
<VAR>k : Type u_2<VAR>Field k<GOAL>normUnit PowerSeries.X = 1
<VAR>k : Type u_2<VAR>Field k<GOAL>PowerSeries.X = normalize PowerSeries.X
<VAR>k : Type u_2<VAR>Field k<VAR>P : Polynomial k<VAR>hP : P ≠ 0<GOAL>Multiset.count PowerSeries.X (UniqueFactorizationMonoid.normalizedFactors ↑P) = Multiset.count Polynomial.X (UniqueFactorizationMonoid.normalizedFactors P)
<VAR>k : Type u_2<VAR>Field k<GOAL>RingHom.ker (PowerSeries.constantCoeff k) = LocalRing.maximalIdeal (PowerSeries k)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>pb : PowerBasis R S<GOAL>(Algebra.norm R) pb.gen = (-1) ^ pb.dim * (minpoly R pb.gen).coeff 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>F : Type u_6<VAR>Field F<VAR>Algebra R F<VAR>pb : PowerBasis R S<VAR>hf : Polynomial.Splits (algebraMap R F) (minpoly R pb.gen)<GOAL>(algebraMap R F) ((Algebra.norm R) pb.gen) = ((minpoly R pb.gen).aroots F).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>Nontrivial S<VAR>Module.Free R S<VAR>Module.Finite R S<GOAL>(Algebra.norm R) 0 = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>x : S<GOAL>(Algebra.norm R) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>x : S<GOAL>(Algebra.norm R) x ≠ 0 ↔ x ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>IsDomain R<VAR>IsDomain S<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>x : S<GOAL>LinearMap.det ((LinearMap.mul R S) x) = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>ι : Type w<VAR>Finite ι<VAR>IsDomain R<VAR>IsDomain S<VAR>b : Basis ι R S<VAR>x : S<GOAL>(Algebra.norm R) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>ι : Type w<VAR>Finite ι<VAR>IsDomain R<VAR>IsDomain S<VAR>b : Basis ι R S<VAR>x : S<GOAL>(Algebra.norm R) x ≠ 0 ↔ x ≠ 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<VAR>x : L<GOAL>(Algebra.norm K) x = (Algebra.norm K) (IntermediateField.AdjoinSimple.gen K x) ^ FiniteDimensional.finrank (↥K⟮x⟯) L
<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.norm K) (IntermediateField.AdjoinSimple.gen K x) = 1
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>Field K<VAR>Field L<VAR>Field F<VAR>Algebra K L<VAR>Algebra K F<VAR>x : L<VAR>hf : Polynomial.Splits (algebraMap K F) (minpoly K x)<GOAL>(algebraMap K F) ((Algebra.norm K) (IntermediateField.AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>F : Type u_6<VAR>Field F<VAR>Algebra R F<VAR>pb : PowerBasis R S<VAR>hE : Polynomial.Splits (algebraMap R F) (minpoly R pb.gen)<VAR>hfx : IsSeparable R pb.gen<GOAL>(algebraMap R F) ((Algebra.norm R) pb.gen) = ∏ σ : S →ₐ[R] F, σ pb.gen
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>Field K<VAR>Field L<VAR>Field F<VAR>Algebra K L<VAR>Algebra K F<VAR>Algebra.IsSeparable K L<VAR>FiniteDimensional K L<VAR>x : L<VAR>hF : Polynomial.Splits (algebraMap K F) (minpoly K x)<GOAL>(algebraMap K F) ((Algebra.norm K) x) = ((minpoly K x).aroots F).prod ^ FiniteDimensional.finrank (↥K⟮x⟯) L
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>Field K<VAR>Field L<VAR>Field F<VAR>Algebra K L<VAR>Algebra K F<VAR>E : Type u_7<VAR>Field E<VAR>Algebra K E<VAR>Algebra L F<VAR>IsScalarTower K L F<VAR>IsAlgClosed E<VAR>Algebra.IsSeparable K F<VAR>FiniteDimensional K F<VAR>pb : PowerBasis K L<GOAL>∏ σ : F →ₐ[K] E, σ ((algebraMap L F) pb.gen) = (∏ σ : L →ₐ[K] E, σ pb.gen) ^ FiniteDimensional.finrank L F
<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>FiniteDimensional K L<VAR>Algebra.IsSeparable K L<VAR>IsAlgClosed E<VAR>x : L<GOAL>(algebraMap K E) ((Algebra.norm K) 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>FiniteDimensional K L<VAR>IsGalois K L<VAR>x : L<GOAL>(algebraMap K L) ((Algebra.norm K) x) = ∏ σ : L ≃ₐ[K] L, σ x
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_4<VAR>L : Type u_5<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Algebra R L<VAR>Algebra R K<VAR>IsScalarTower R K L<VAR>Algebra.IsSeparable K L<VAR>FiniteDimensional K L<VAR>x : L<VAR>hx : IsIntegral R x<GOAL>IsIntegral R ((Algebra.norm K) x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>Ring T<VAR>Algebra R T<VAR>e : S ≃ₐ[R] T<VAR>x : S<GOAL>(Algebra.norm R) (e x) = (Algebra.norm R) x
<VAR>A : Type u_8<VAR>B : Type u_9<VAR>C : Type u_10<VAR>CommRing A<VAR>CommRing B<VAR>Ring 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.norm A) x) = (Algebra.norm B) x
<VAR>A₁ : Type u_8<VAR>B₁ : Type u_9<VAR>A₂ : Type u_10<VAR>B₂ : Type u_11<VAR>CommRing A₁<VAR>Ring B₁<VAR>CommRing A₂<VAR>Ring 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.norm A₁) x = e₁.symm ((Algebra.norm A₂) (e₂ x))
<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>Field K<VAR>Field L<VAR>Field F<VAR>Algebra K L<VAR>Algebra K F<VAR>Algebra L F<VAR>IsScalarTower K L F<VAR>Algebra.IsSeparable K F<VAR>x : F<GOAL>(Algebra.norm K) ((Algebra.norm L) x) = (Algebra.norm K) x
<VAR>R : Type u_1<VAR>Ring R<VAR>u : Rˣ<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) (PowerSeries.invUnitsSub u) = 1 /ₚ u ^ (n + 1)
<VAR>R : Type u_1<VAR>Ring R<VAR>u : Rˣ<GOAL>(PowerSeries.constantCoeff R) (PowerSeries.invUnitsSub u) = 1 /ₚ u
<VAR>R : Type u_1<VAR>Ring R<VAR>u : Rˣ<GOAL>PowerSeries.invUnitsSub u * PowerSeries.X = PowerSeries.invUnitsSub u * (PowerSeries.C R) ↑u - 1
<VAR>R : Type u_1<VAR>Ring R<VAR>u : Rˣ<GOAL>PowerSeries.invUnitsSub u * ((PowerSeries.C R) ↑u - PowerSeries.X) = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>u : Rˣ<GOAL>(PowerSeries.map f) (PowerSeries.invUnitsSub u) = PowerSeries.invUnitsSub ((Units.map ↑f) u)
<VAR>S : Type u_1<VAR>CommRing S<GOAL>PowerSeries.mk 1 * (1 - PowerSeries.X) = 1
<VAR>S : Type u_1<VAR>CommRing S<VAR>d : ℕ<GOAL>PowerSeries.mk 1 ^ (d + 1) = PowerSeries.mk fun n => ↑((d + n).choose d)
<VAR>S : Type u_1<VAR>CommRing S<VAR>d : ℕ<GOAL>↑(PowerSeries.invOneSubPow d) = PowerSeries.mk fun n => ↑((d + n).choose d)
<VAR>S : Type u_1<VAR>CommRing S<GOAL>↑(PowerSeries.invOneSubPow 0) = PowerSeries.invUnitsSub 1
<VAR>S : Type u_1<VAR>CommRing S<VAR>d : ℕ<GOAL>PowerSeries.invOneSubPow d = (Units.mkOfMulEqOne (1 - PowerSeries.X) (PowerSeries.mk 1) ⋯)⁻¹ ^ (d + 1)
<VAR>S : Type u_1<VAR>CommRing S<VAR>d : ℕ<GOAL>(PowerSeries.invOneSubPow d).inv = (1 - PowerSeries.X) ^ (d + 1)
<VAR>A : Type u_1<VAR>Ring A<VAR>Algebra ℚ A<VAR>n : ℕ<GOAL>(PowerSeries.coeff A n) (PowerSeries.exp A) = (algebraMap ℚ A) (1 / ↑n.factorial)
<VAR>A : Type u_1<VAR>Ring A<VAR>Algebra ℚ A<GOAL>(PowerSeries.constantCoeff A) (PowerSeries.exp A) = 1
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>Ring A<VAR>Ring A'<VAR>Algebra ℚ A<VAR>Algebra ℚ A'<VAR>f : A →+* A'<GOAL>(PowerSeries.map f) (PowerSeries.exp A) = PowerSeries.exp A'
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>Ring A<VAR>Ring A'<VAR>Algebra ℚ A<VAR>Algebra ℚ A'<VAR>f : A →+* A'<GOAL>(PowerSeries.map f) (PowerSeries.sin A) = PowerSeries.sin A'
<VAR>A : Type u_1<VAR>A' : Type u_2<VAR>Ring A<VAR>Ring A'<VAR>Algebra ℚ A<VAR>Algebra ℚ A'<VAR>f : A →+* A'<GOAL>(PowerSeries.map f) (PowerSeries.cos A) = PowerSeries.cos A'
<VAR>A : Type u_1<VAR>CommRing A<VAR>Algebra ℚ A<VAR>a b : A<GOAL>(PowerSeries.rescale a) (PowerSeries.exp A) * (PowerSeries.rescale b) (PowerSeries.exp A) = (PowerSeries.rescale (a + b)) (PowerSeries.exp A)
<VAR>A : Type u_1<VAR>CommRing A<VAR>Algebra ℚ A<GOAL>PowerSeries.exp A * PowerSeries.evalNegHom (PowerSeries.exp A) = 1
<VAR>A : Type u_1<VAR>CommRing A<VAR>Algebra ℚ A<VAR>k : ℕ<GOAL>PowerSeries.exp A ^ k = (PowerSeries.rescale ↑k) (PowerSeries.exp A)
<VAR>A : Type u_1<VAR>CommRing A<VAR>Algebra ℚ A<VAR>n : ℕ<GOAL>∑ k ∈ Finset.range n, PowerSeries.exp A ^ k = PowerSeries.mk fun p => ∑ k ∈ Finset.range n, ↑k ^ p * (algebraMap ℚ A) (↑p.factorial)⁻¹
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N₁ N₂ : Submodule R M<VAR>h : N₁ ≤ N₂<VAR>h' : N₂.FG<GOAL>Submodule.map (LocalRing.maximalIdeal R • N₂).mkQ N₁ = Submodule.map (LocalRing.maximalIdeal R • N₂).mkQ N₂ ↔ N₁ = N₂
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>Module.Finite R M<GOAL>Submodule.map (LocalRing.maximalIdeal R • ⊤).mkQ N = ⊤ ↔ N = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>Module.Finite R M<GOAL>Submodule.map ((TensorProduct.mk R (LocalRing.ResidueField R) M) 1) N = ⊤ ↔ N = ⊤
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<GOAL>Subsingleton (TensorProduct R (LocalRing.ResidueField R) M) ↔ Subsingleton M
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<VAR>ι : Type u_3<VAR>f : ι → M<VAR>b : Basis ι (LocalRing.ResidueField R) (TensorProduct R (LocalRing.ResidueField R) M)<VAR>hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i<GOAL>Submodule.span R (Set.range f) = ⊤
<VAR>R : Type u_7<VAR>CommRing R<VAR>M₁ : Type u_1<VAR>M₂ : Type u_2<VAR>M₃ : Type u_3<VAR>N₁ : Type u_4<VAR>N₂ : Type u_5<VAR>N₃ : Type u_6<VAR>AddCommGroup M₁<VAR>Module R M₁<VAR>AddCommGroup M₂<VAR>Module R M₂<VAR>AddCommGroup M₃<VAR>Module R M₃<VAR>AddCommGroup N₁<VAR>Module R N₁<VAR>AddCommGroup N₂<VAR>Module R N₂<VAR>AddCommGroup N₃<VAR>Module R N₃<VAR>f₁ : M₁ →ₗ[R] M₂<VAR>f₂ : M₂ →ₗ[R] M₃<VAR>g₁ : N₁ →ₗ[R] N₂<VAR>g₂ : N₂ →ₗ[R] N₃<VAR>hfexact : Function.Exact ⇑f₁ ⇑f₂<VAR>hfsurj : Function.Surjective ⇑f₂<VAR>hgexact : Function.Exact ⇑g₁ ⇑g₂<VAR>hgsurj : Function.Surjective ⇑g₂<VAR>hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)<VAR>hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)<GOAL>Function.Injective ⇑(LinearMap.lTensor M₃ g₁)
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.FinitePresentation R M<VAR>H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype (LocalRing.maximalIdeal R)))<GOAL>Module.Free R M
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>P : Type u_2<VAR>AddCommGroup P<VAR>Module R P<VAR>Module.FinitePresentation R P<VAR>Module.Flat R P<GOAL>Module.Free R P
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>P : Type u_4<VAR>AddCommGroup P<VAR>Module R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>hg : Function.Surjective ⇑g<VAR>h : Function.Exact ⇑f ⇑g<VAR>Module.Finite R M<VAR>Module.Finite R N<VAR>Module.Free R N<VAR>hf : Function.Injective ⇑(LinearMap.lTensor (LocalRing.ResidueField R) f)<GOAL>Module.Free R P
<VAR>R : Type u_1<VAR>CommRing R<VAR>LocalRing R<VAR>M : Type u_2<VAR>N : Type u_3<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>Module.Finite R M<VAR>Module.Finite R N<VAR>Module.Free R N<VAR>l : M →ₗ[R] N<GOAL>(∃ l', l' ∘ₗ l = LinearMap.id) ↔ Function.Injective ⇑(LinearMap.lTensor (LocalRing.ResidueField R) l)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>self : IsNoetherian R M<VAR>s : Submodule R M<GOAL>s.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>IsNoetherian R M ↔ ∀ (s : Submodule R M), s.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>IsNoetherian R ↥N ↔ ∀ s ≤ N, s.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>IsNoetherian R ↥N ↔ ∀ (s : Submodule R M), (N ⊓ s).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<GOAL>IsNoetherian R ↥N ↔ ∀ (s : Submodule R M), (s ⊓ N).FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s t : Submodule R M<VAR>ht : IsNoetherian R ↥t<VAR>h : s ≤ t<GOAL>IsNoetherian R ↥s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R P<VAR>f : M →ₗ[R] P<VAR>hf : LinearMap.range f = ⊤<VAR>IsNoetherian R M<GOAL>IsNoetherian R P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R P<VAR>f : M ≃ₗ[R] P<VAR>IsNoetherian R M<GOAL>IsNoetherian R P
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>IsNoetherian R ↥⊤ ↔ IsNoetherian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R P<VAR>IsNoetherian R P<VAR>f : M →ₗ[R] P<VAR>hf : Function.Injective ⇑f<GOAL>IsNoetherian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R P<VAR>IsNoetherian R P<VAR>N : Submodule R M<VAR>f : M →ₗ[R] P<VAR>hf : Function.Injective ⇑f<GOAL>N.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>Module R M<VAR>Module R N<VAR>IsNoetherian R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Injective ⇑f<GOAL>Module.Finite R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R P<VAR>IsNoetherian R P<VAR>f : M →ₗ[R] P<VAR>hf : LinearMap.ker f = ⊥<GOAL>IsNoetherian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup P<VAR>Module R M<VAR>Module R P<VAR>IsNoetherian R P<VAR>N : Submodule R M<VAR>f : M →ₗ[R] P<VAR>hf : LinearMap.ker f = ⊥<GOAL>N.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>IsNoetherian R M ↔ WellFounded fun x x_1 => x > x_1
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>IsNoetherian R M<GOAL>WellFounded fun x x_1 => x > x_1
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>(∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>(∀ (f : ℕ →o Submodule R M), ∃ n, ∀ (m : ℕ), n ≤ m → f n = f m) ↔ IsNoetherian R M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>IsNoetherian R M<VAR>f : ℕ →o Submodule R M<GOAL>Filter.EventuallyConst (⇑f) Filter.atTop
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>IsNoetherian R M<VAR>P : Submodule R M → Prop<VAR>hgt : ∀ (I : Submodule R M), (∀ J > I, P J) → P I<VAR>I : Submodule R M<GOAL>P I
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>ι : Type u_4<VAR>N : ι → Submodule R M<VAR>h : CompleteLattice.Independent N<GOAL>{i | N i ≠ ⊥}.Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>Nontrivial R<VAR>ι : Type u_4<VAR>v : ι → M<VAR>hv : LinearIndependent R v<GOAL>Finite ι
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>Nontrivial R<VAR>s : Set M<VAR>hi : LinearIndependent (ι := { x // x ∈ s }) R Subtype.val<GOAL>s.Finite
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>P : Type u_3<VAR>N : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>AddCommGroup P<VAR>Module R P<VAR>IsNoetherian R M<VAR>IsNoetherian R P<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>h : LinearMap.range f = LinearMap.ker g<GOAL>IsNoetherian R N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>f : M →ₗ[R] M<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, Disjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>f : M →ₗ[R] M<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, ⨆ m, LinearMap.ker (f ^ m) = LinearMap.ker (f ^ n)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>IsNoetherian R M<VAR>i f : N →ₗ[R] M<VAR>hi : Function.Injective ⇑i<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>N : Submodule R M<VAR>f : ↥N →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>s : Function.Surjective ⇑f<GOAL>Function.Injective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>f : M →ₗ[R] M<VAR>s : Function.Surjective ⇑f<GOAL>Function.Bijective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherian R M<VAR>f : ℕ → Submodule R M<VAR>h : ∀ (n : ℕ), Disjoint ((partialSups f) n) (f (n + 1))<GOAL>∃ n, ∀ (m : ℕ), n ≤ m → f m = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>IsNoetherian R M<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<GOAL>Subsingleton N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>IsNoetherian R M<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<GOAL>∀ (x : N), (IsNoetherian.equivPUnitOfProdInjective f i) x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type w<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup N<VAR>Module R N<VAR>IsNoetherian R M<VAR>f : M × N →ₗ[R] M<VAR>i : Function.Injective ⇑f<GOAL>∀ (x : PUnit.{w + 1}), (IsNoetherian.equivPUnitOfProdInjective f i).symm x = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>IsNoetherianRing R ↔ IsNoetherian R R
<VAR>R : Type u_1<VAR>Semiring R<GOAL>IsNoetherianRing R ↔ ∀ (I : Ideal R), I.FG
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<VAR>h : IsNoetherian R M<GOAL>IsNoetherian R ↥N
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>SMul R S<VAR>Module S M<VAR>Module R M<VAR>IsScalarTower R S M<VAR>h : IsNoetherian R M<GOAL>IsNoetherian S M
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>I : IsNoetherianRing R<VAR>hN : N.FG<GOAL>IsNoetherian R ↥N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>A : Set M<VAR>hA : A.Finite<GOAL>IsNoetherian R ↥(Submodule.span R A)
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Type u_2<VAR>Ring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>H : IsNoetherianRing R<GOAL>IsNoetherianRing S
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Type u_2<VAR>Ring S<VAR>f : R ≃+* S<VAR>IsNoetherianRing R<GOAL>IsNoetherianRing S
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsNoetherianRing R<GOAL>IsNilpotent (nilradical R)
<VAR>R : Type u_1<VAR>Semiring R<VAR>φ : PowerSeries R<GOAL>(∃ n, (PowerSeries.coeff R n) φ ≠ 0) ↔ φ ≠ 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>PowerSeries.order 0 = ⊤