ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f : M →ₗ[R] M<VAR>p : Submodule R M<VAR>hf : Set.MapsTo ⇑f ↑p ↑p<VAR>hnil : IsNilpotent f<GOAL>IsNilpotent (f.restrict hf)
<VAR>R : Type u_1<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : Module.End R M<VAR>p : Submodule R M<VAR>hp : p ≤ Submodule.comap f p<VAR>hnp : IsNilpotent f<GOAL>IsNilpotent (p.mapQ p f hp)
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>GCDMonoid R<VAR>p q : R<VAR>hp : p ≠ 0<GOAL>gcd p q ≠ 0
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>GCDMonoid R<VAR>p q : R<VAR>hp : q ≠ 0<GOAL>gcd p q ≠ 0
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>GCDMonoid R<VAR>p q : R<VAR>hp : p ≠ 0<GOAL>p / gcd p q ≠ 0
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>GCDMonoid R<VAR>p q : R<VAR>hq : q ≠ 0<GOAL>q / gcd p q ≠ 0
<VAR>R : Type u_1<VAR>EuclideanDomain R<VAR>GCDMonoid R<VAR>p q : R<VAR>hq : q ≠ 0<GOAL>IsCoprime (p / gcd p q) (q / gcd p q)
<VAR>α : Type u_1<VAR>EuclideanDomain α<VAR>DecidableEq α<VAR>x y : α<GOAL>Ideal.span {EuclideanDomain.gcd x y} = Ideal.span {x, y}
<VAR>α : Type u_1<VAR>EuclideanDomain α<VAR>DecidableEq α<VAR>x y : α<GOAL>IsUnit (EuclideanDomain.gcd x y) ↔ IsCoprime x y
<VAR>α : Type u_1<VAR>EuclideanDomain α<VAR>x y : α<VAR>nonzero : ¬(x = 0 ∧ y = 0)<VAR>H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬z ∣ y<GOAL>IsCoprime x y
<VAR>α : Type u_1<VAR>EuclideanDomain α<VAR>x y : α<VAR>h : Irreducible x<GOAL>x ∣ y ∨ IsCoprime x y
<VAR>R : Type u_1<VAR>x : R<VAR>Ring R<VAR>h : IsNilpotent x<GOAL>IsNilpotent (-x)
<VAR>R : Type u_1<VAR>x : R<VAR>Ring R<GOAL>IsNilpotent (-x) ↔ IsNilpotent x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>MonoidWithZero R<VAR>MonoidWithZero S<VAR>MulActionWithZero R S<VAR>SMulCommClass R S S<VAR>IsScalarTower R S S<VAR>a : S<VAR>ha : IsNilpotent a<VAR>t : R<GOAL>IsNilpotent (t • a)
<VAR>R : Type u_1<VAR>Ring R<VAR>r : R<VAR>hnil : IsNilpotent r<GOAL>IsUnit (r - 1)
<VAR>R : Type u_1<VAR>Ring R<VAR>r : R<VAR>hnil : IsNilpotent r<GOAL>IsUnit (1 - r)
<VAR>R : Type u_1<VAR>Ring R<VAR>r : R<VAR>hnil : IsNilpotent r<GOAL>IsUnit (r + 1)
<VAR>R : Type u_1<VAR>Ring R<VAR>r : R<VAR>hnil : IsNilpotent r<GOAL>IsUnit (1 + r)
<VAR>R : Type u_1<VAR>Ring R<VAR>r u : R<VAR>hnil : IsNilpotent r<VAR>hu : IsUnit u<VAR>h_comm : Commute r u<GOAL>IsUnit (u + r)
<VAR>R : Type u_1<VAR>Ring R<VAR>r u : R<VAR>hnil : IsNilpotent r<VAR>hu : IsUnit u<VAR>h_comm : Commute r u<GOAL>IsUnit (r + u)
<VAR>R : Type u_1<VAR>CommMonoidWithZero R<VAR>y : R<VAR>hy : Prime y<GOAL>IsRadical y
<VAR>R : Type u_1<VAR>MonoidWithZero R<GOAL>IsRadical 0 ↔ IsReduced R
<VAR>R : Type u_1<VAR>MonoidWithZero R<VAR>k : ℕ<VAR>hk : 1 < k<GOAL>IsReduced R ↔ ∀ (x : R), x ^ k = 0 → x = 0
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x y : R<VAR>hy : IsRadical y<VAR>h0 : y ≠ 0<VAR>hxy : x ∣ y<GOAL>IsRadical x
<VAR>R : Type u_1<VAR>x y : R<VAR>Semiring R<VAR>h_comm : Commute x y<VAR>m n k : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<VAR>h : m + n ≤ k + 1<GOAL>(x + y) ^ k = 0
<VAR>R : Type u_1<VAR>x y : R<VAR>Semiring R<VAR>h_comm : Commute x y<VAR>m n : ℕ<VAR>hx : x ^ m = 0<VAR>hy : y ^ n = 0<GOAL>(x + y) ^ (m + n - 1) = 0
<VAR>R : Type u_1<VAR>x y : R<VAR>Semiring R<VAR>h_comm : Commute x y<VAR>hx : IsNilpotent x<VAR>hy : IsNilpotent y<GOAL>IsNilpotent (x + y)
<VAR>R : Type u_1<VAR>Semiring R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → R<VAR>hnp : ∀ i ∈ s, IsNilpotent (f i)<VAR>h_comm : ∀ (i j : ι), i ∈ s → j ∈ s → Commute (f i) (f j)<GOAL>IsNilpotent (∑ i ∈ s, f i)
<VAR>R : Type u_1<VAR>x y : R<VAR>Semiring R<VAR>h_comm : Commute x y<VAR>hy : y ∈ nonZeroDivisorsLeft R<GOAL>IsNilpotent (x * y) ↔ IsNilpotent x
<VAR>R : Type u_1<VAR>x y : R<VAR>Semiring R<VAR>h_comm : Commute x y<VAR>hx : x ∈ nonZeroDivisorsRight R<GOAL>IsNilpotent (x * y) ↔ IsNilpotent y
<VAR>R : Type u_1<VAR>x y : R<VAR>Ring R<VAR>h_comm : Commute x y<VAR>hx : IsNilpotent x<VAR>hy : IsNilpotent y<GOAL>IsNilpotent (x - y)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → R<VAR>hnp : ∀ i ∈ s, IsNilpotent (f i)<GOAL>IsNilpotent (∑ i ∈ s, f i)
<VAR>R : Type u_3<VAR>M : Type u_4<VAR>MonoidWithZero R<VAR>Zero M<VAR>MulActionWithZero R M<VAR>Nontrivial M<VAR>NoZeroSMulDivisors R M<GOAL>IsReduced R
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>self : Derivation R A M<VAR>a b : A<GOAL>↑self (a * b) = a • ↑self b + b • ↑self a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>self : Derivation R A M<GOAL>↑self 1 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<GOAL>(↑D).toFun = ⇑D
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>f : A →ₗ[R] M<VAR>h₁ : f 1 = 0<VAR>h₂ : ∀ (a b : A), f (a * b) = a • f b + b • f a<GOAL>⇑{ toLinearMap := f, map_one_eq_zero' := h₁, leibniz' := h₂ } = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>f : Derivation R A M<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<VAR>H : ∀ (a : A), D1 a = D2 a<GOAL>D1 = D2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<VAR>h : D1 = D2<VAR>a : A<GOAL>D1 a = D2 a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>a b : A<GOAL>D (a + b) = D a + D b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<GOAL>D 0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>r : R<VAR>a : A<GOAL>D (r • a) = r • D a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>a b : A<GOAL>D (a * b) = a • D b + b • D a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>S : Type u_5<VAR>SMul S A<VAR>SMul S M<VAR>LinearMap.CompatibleSMul A M S R<VAR>D : Derivation R A M<VAR>r : S<VAR>a : A<GOAL>D (r • a) = r • D a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<GOAL>D 1 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>r : R<GOAL>D ((algebraMap R A) r) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>n : ℕ<GOAL>D ↑n = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>a : A<VAR>n : ℕ<GOAL>D (a ^ n) = n • a ^ (n - 1) • D a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>P : Polynomial R<VAR>x : A<GOAL>D ((Polynomial.aeval x) P) = (Polynomial.aeval x) (Polynomial.derivative P) • D x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<VAR>s : Set A<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<GOAL>Set.EqOn ⇑D1 ⇑D2 ↑(Algebra.adjoin R s)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<VAR>s : Set A<VAR>hs : Algebra.adjoin R s = ⊤<VAR>h : Set.EqOn (⇑D1) (⇑D2) s<GOAL>D1 = D2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<GOAL>⇑0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<GOAL>↑0 = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>a : A<GOAL>0 a = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<GOAL>⇑(D1 + D2) = ⇑D1 + ⇑D2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<GOAL>↑(D1 + D2) = ↑D1 + ↑D2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<VAR>a : A<GOAL>(D1 + D2) a = D1 a + D2 a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>S : Type u_5<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass R S M<VAR>SMulCommClass S A M<VAR>r : S<VAR>D : Derivation R A M<GOAL>⇑(r • D) = r • ⇑D
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>S : Type u_5<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass R S M<VAR>SMulCommClass S A M<VAR>r : S<VAR>D : Derivation R A M<GOAL>↑(r • D) = r • ↑D
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>a : A<VAR>S : Type u_5<VAR>Monoid S<VAR>DistribMulAction S M<VAR>SMulCommClass R S M<VAR>SMulCommClass S A M<VAR>r : S<VAR>D : Derivation R A M<GOAL>(r • D) a = r • D a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>Module A N<VAR>Module R N<VAR>IsScalarTower R A M<VAR>IsScalarTower R A N<VAR>f : M →ₗ[A] N<GOAL>↑(f.compDer D) = ↑R f ∘ₗ ↑D
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>Module A N<VAR>Module R N<VAR>IsScalarTower R A M<VAR>IsScalarTower R A N<VAR>f : M →ₗ[A] N<GOAL>⇑(f.compDer D) = ⇑(↑R f ∘ₗ ↑D)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>Module A N<VAR>Module R N<VAR>IsScalarTower R A M<VAR>IsScalarTower R A N<VAR>f : M →ₗ[A] N<GOAL>Derivation.llcomp f = f.compDer
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>Module A N<VAR>Module R N<VAR>IsScalarTower R A M<VAR>IsScalarTower R A N<VAR>e : M ≃ₗ[A] N<GOAL>↑(e.compDer D) = ↑R ↑e ∘ₗ ↑D
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>N : Type u_5<VAR>AddCommMonoid N<VAR>Module A N<VAR>Module R N<VAR>IsScalarTower R A M<VAR>IsScalarTower R A N<VAR>e : M ≃ₗ[A] N<GOAL>⇑(e.compDer D) = ⇑(↑R ↑e ∘ₗ ↑D)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>CommSemiring B<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Algebra R B<VAR>Module A M<VAR>Module B M<VAR>Module R M<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>IsScalarTower A B M<VAR>d : Derivation R B M<GOAL>∀ (a : A), (Derivation.compAlgebraMap A d) a = d ((algebraMap A B) a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>S : Type u_5<VAR>CommSemiring S<VAR>Algebra S A<VAR>Module S M<VAR>LinearMap.CompatibleSMul A M R S<VAR>d : Derivation S A M<GOAL>⇑(Derivation.restrictScalars R d) = ⇑d
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_4<VAR>CommSemiring R<VAR>CommSemiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>S : Type u_5<VAR>CommSemiring S<VAR>Algebra S A<VAR>Module S M<VAR>LinearMap.CompatibleSMul A M R S<VAR>d : Derivation S A M<VAR>x : A<GOAL>(Derivation.restrictScalars R d) x = d x
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>CommSemiring A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCancelCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>D : A →ₗ[R] M<VAR>h : ∀ (a b : A), D (a * b) = a • D b + b • D a<GOAL>⇑(Derivation.mk' D h) = ⇑D
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>A : Type u_2<VAR>CommSemiring A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCancelCommMonoid M<VAR>Module R M<VAR>Module A M<VAR>D : A →ₗ[R] M<VAR>h : ∀ (a b : A), D (a * b) = a • D b + b • D a<GOAL>↑(Derivation.mk' D h) = D
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>a : A<GOAL>D (-a) = -D a
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>a b : A<GOAL>D (a - b) = D a - D b
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>n : ℤ<GOAL>D ↑n = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>a b : A<VAR>h : a * b = 1<GOAL>D a = -a ^ 2 • D b
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>a : A<VAR>Invertible a<GOAL>D ⅟a = -⅟a ^ 2 • D a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>K : Type u_4<VAR>Field K<VAR>Module K M<VAR>Algebra R K<VAR>D : Derivation R K M<VAR>a : K<GOAL>D a⁻¹ = -a⁻¹ ^ 2 • D a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>K : Type u_4<VAR>Field K<VAR>Module K M<VAR>Algebra R K<VAR>D : Derivation R K M<VAR>a b : K<GOAL>D (a / b) = b⁻¹ ^ 2 • (b • D a - a • D b)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>K : Type u_4<VAR>Field K<VAR>Module K M<VAR>Algebra R K<VAR>D : Derivation R K M<VAR>a b : K<VAR>h : D b = 0<GOAL>D (a / b) = b⁻¹ • D a
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module R M<VAR>K : Type u_4<VAR>Field K<VAR>Module K M<VAR>Algebra R K<VAR>D : Derivation R K M<VAR>a : K<VAR>n : ℤ<GOAL>D (a ^ n) = n • a ^ (n - 1) • D a
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<GOAL>⇑(-D) = -⇑D
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<GOAL>↑(-D) = -↑D
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D : Derivation R A M<VAR>a : A<GOAL>(-D) a = -D a
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<GOAL>⇑(D1 - D2) = ⇑D1 - ⇑D2
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<GOAL>↑(D1 - D2) = ↑D1 - ↑D2
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>Module A M<VAR>Module R M<VAR>D1 D2 : Derivation R A M<VAR>a : A<GOAL>(D1 - D2) a = D1 a - D2 a
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>h : I ≤ ⊥.jacobson<GOAL>IsLocalRingHom (Ideal.Quotient.mk I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>self : HenselianRing R I<GOAL>I ≤ ⊥.jacobson
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>self : HenselianRing R I<VAR>f : R[X]<GOAL>f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ I → IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f))) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>self : HenselianLocalRing R<VAR>f : R[X]<GOAL>f.Monic → ∀ (a₀ : R), Polynomial.eval a₀ f ∈ LocalRing.maximalIdeal R → IsUnit (Polynomial.eval a₀ (Polynomial.derivative f)) → ∃ a, f.IsRoot a ∧ a - a₀ ∈ LocalRing.maximalIdeal R
<VAR>R : Type u<VAR>CommRing R<VAR>LocalRing R<GOAL>[HenselianLocalRing R, ∀ (f : R[X]), f.Monic → ∀ (a₀ : LocalRing.ResidueField R), (Polynomial.aeval a₀) f = 0 → (Polynomial.aeval a₀) (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (LocalRing.residue R) a = a₀, ∀ {K : Type u} [inst : Field K] (φ : R →+* K), Function.Surjective ⇑φ → ∀ (f : R[X]), f.Monic → ∀ (a₀ : K), Polynomial.eval₂ φ a₀ f = 0 → Polynomial.eval₂ φ a₀ (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>α : Type u_2<VAR>DecidableEq α<VAR>x y a : R<VAR>s : Finset α<VAR>p : α → R<VAR>hp : ∀ i ∈ s, Prime (p i)<VAR>hx : x * y = a * ∏ i ∈ s, p i<GOAL>∃ t u b c, t ∪ u = s ∧ Disjoint t u ∧ a = b * c ∧ x = b * ∏ i ∈ t, p i ∧ y = c * ∏ i ∈ u, p i
<VAR>R : Type u_1<VAR>CancelCommMonoidWithZero R<VAR>x y a p : R<VAR>n : ℕ<VAR>hp : Prime p<VAR>hx : x * y = a * p ^ n<GOAL>∃ i j b c, i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j
<VAR>α : Type u_1<VAR>CommRing α<VAR>p : α<VAR>hp : Prime p<GOAL>Prime (-p)
<VAR>α : Type u_1<VAR>CommRing α<VAR>LinearOrder α<VAR>p : α<VAR>hp : Prime p<GOAL>Prime |p|
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>self : AddOreLocalization.AddOreSet S<VAR>r : R<VAR>s : ↥S<GOAL>↑(AddOreLocalization.AddOreSet.oreSubtra r s) + r = AddOreLocalization.AddOreSet.oreMin r s + ↑s
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>self : AddOreLocalization.AddOreSet S<VAR>r₁ r₂ : R<VAR>s : ↥S<GOAL>r₁ + ↑s = r₂ + ↑s → ∃ s', ↑s' + r₁ = ↑s' + r₂
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>self : OreLocalization.OreSet S<VAR>r : R<VAR>s : ↥S<GOAL>↑(OreLocalization.OreSet.oreDenom r s) * r = OreLocalization.OreSet.oreNum r s * ↑s
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>self : OreLocalization.OreSet S<VAR>r₁ r₂ : R<VAR>s : ↥S<GOAL>r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r₁ r₂ : R<VAR>s : ↥S<VAR>h : r₁ + ↑s = r₂ + ↑s<GOAL>∃ s', ↑s' + r₁ = ↑s' + r₂
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r₁ r₂ : R<VAR>s : ↥S<VAR>h : r₁ * ↑s = r₂ * ↑s<GOAL>∃ s', ↑s' * r₁ = ↑s' * r₂
<VAR>R : Type u_1<VAR>AddMonoid R<VAR>S : AddSubmonoid R<VAR>AddOreLocalization.AddOreSet S<VAR>r : R<VAR>s : ↥S<GOAL>↑(AddOreLocalization.oreSubtra r s) + r = AddOreLocalization.oreMin r s + ↑s
<VAR>R : Type u_1<VAR>Monoid R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r : R<VAR>s : ↥S<GOAL>↑(OreLocalization.oreDenom r s) * r = OreLocalization.oreNum r s * ↑s
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Submonoid R<GOAL>Nonempty (OreLocalization.OreSet S) ↔ (∀ (r₁ r₂ : R) (s : ↥S), r₁ * ↑s = r₂ * ↑s → ∃ s', ↑s' * r₁ = ↑s' * r₂) ∧ ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
<VAR>R : Type u_1<VAR>Ring R<VAR>NoZeroDivisors R<VAR>S : Submonoid R<GOAL>Nonempty (OreLocalization.OreSet S) ↔ ∀ (r : R) (s : ↥S), ∃ r' s', ↑s' * r = r' * ↑s
<VAR>R : Type u_7<VAR>S : Type u_8<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>self : PowerBasis R S<VAR>i : Fin self.dim<GOAL>self.basis i = self.gen ^ ↑i
<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>⇑pb.basis = fun i => pb.gen ^ ↑i
<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>Module.Finite R S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>StrongRankCondition R<VAR>pb : PowerBasis R S<GOAL>FiniteDimensional.finrank R S = pb.dim
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>x y : S<VAR>d : ℕ<GOAL>y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.degree < ↑d ∧ y = (Polynomial.aeval x) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>x y : S<VAR>d : ℕ<VAR>hd : d ≠ 0<GOAL>y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.natDegree < d ∧ y = (Polynomial.aeval x) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>Nontrivial S<VAR>pb : PowerBasis R S<GOAL>pb.dim ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>Nontrivial S<VAR>pb : PowerBasis R S<GOAL>0 < pb.dim
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>Nontrivial S<VAR>pb : PowerBasis R S<VAR>y : S<GOAL>∃ f, f.natDegree < pb.dim ∧ y = (Polynomial.aeval pb.gen) f
<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<VAR>y : S<GOAL>∃ f, y = (Polynomial.aeval pb.gen) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>S' : Type u_7<VAR>Semiring S'<VAR>Algebra R S'<VAR>pb : PowerBasis R S<VAR>f g : S →ₐ[R] S'<VAR>h : f pb.gen = g pb.gen<GOAL>f = g
<VAR>A : Type u_4<VAR>B : Type u_5<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>pb : PowerBasis A B<VAR>b : B<GOAL>∃ a, b ≡ (algebraMap A B) a [SMOD Ideal.span {pb.gen}]
<VAR>A : Type u_4<VAR>B : Type u_5<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>pb : PowerBasis A B<VAR>b : B<GOAL>∃ a, pb.gen ∣ b - (algebraMap A B) a
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>pb : PowerBasis A S<GOAL>(Polynomial.aeval pb.gen) pb.minpolyGen = 0
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>pb : PowerBasis A S<GOAL>pb.minpolyGen.Monic
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>pb : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>root : (Polynomial.aeval pb.gen) p = 0<GOAL>pb.dim ≤ p.natDegree
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>h : PowerBasis A S<VAR>p : A[X]<VAR>ne_zero : p ≠ 0<VAR>root : (Polynomial.aeval h.gen) p = 0<GOAL>↑h.dim ≤ p.degree
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>Nontrivial A<VAR>pb : PowerBasis A S<GOAL>pb.minpolyGen.degree = ↑pb.dim
<VAR>S : Type u_2<VAR>Ring S<VAR>A : Type u_4<VAR>CommRing A<VAR>Algebra A S<VAR>Nontrivial A<VAR>pb : PowerBasis A S<GOAL>pb.minpolyGen.natDegree = pb.dim