ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>f : M →ₗ[R] M'<VAR>hf : Function.Injective ⇑f<GOAL>associatedPrimes R M ⊆ associatedPrimes R M'
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>M' : Type u_3<VAR>AddCommGroup M'<VAR>Module R M'<VAR>l : M ≃ₗ[R] M'<GOAL>associatedPrimes R M = associatedPrimes R M'
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>Subsingleton M<GOAL>associatedPrimes R M = ∅
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<VAR>Nontrivial M<GOAL>(associatedPrimes R M).Nonempty
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<GOAL>⋃ p ∈ associatedPrimes R M, ↑p = {r | ∃ x, x ≠ 0 ∧ r • x = 0}
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>AddCommGroup M<VAR>Module R M<VAR>h : IsAssociatedPrime I M<GOAL>⊤.annihilator ≤ I
<VAR>R : Type u_1<VAR>CommRing R<VAR>I J : Ideal R<VAR>hI : I.IsPrimary<VAR>h : IsAssociatedPrime J (R ⧸ I)<GOAL>J = I.radical
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Ideal R<VAR>IsNoetherianRing R<VAR>hI : I.IsPrimary<GOAL>associatedPrimes R (R ⧸ I) = {I.radical}
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<GOAL>a • S = Ideal.map (MulSemiringAction.toRingHom M R a) S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>m : M<VAR>r : R<VAR>S : Ideal R<GOAL>r ∈ S → m • r ∈ m • S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<GOAL>a • ⊥ = ⊥
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Ideal R<GOAL>a • (S ⊔ T) = a • S ⊔ a • T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Monoid M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>s : Set R<GOAL>a • Ideal.span s = Ideal.span (a • s)
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<GOAL>a • S = Ideal.comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) a)) S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x : R<GOAL>a • x ∈ a • S ↔ x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x : R<GOAL>x ∈ a • S ↔ a⁻¹ • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>ha : Function.Surjective fun r => a • r<GOAL>(a • S).toAddSubmonoid = a • S.toAddSubmonoid
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>ha : Function.Surjective fun r => a • r<GOAL>Submodule.toAddSubgroup (a • S) = a • Submodule.toAddSubgroup S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S : Ideal R<VAR>x : R<GOAL>x ∈ a⁻¹ • S ↔ a • x ∈ S
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Ideal R<GOAL>a • S ≤ a • T ↔ S ≤ T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Ideal R<GOAL>a • S ≤ T ↔ S ≤ a⁻¹ • T
<VAR>M : Type u_1<VAR>R : Type u_2<VAR>Group M<VAR>CommRing R<VAR>MulSemiringAction M R<VAR>a : M<VAR>S T : Ideal R<GOAL>S ≤ a • T ↔ a⁻¹ • S ≤ T
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>AlgebraicIndependent R x ↔ RingHom.ker (MvPolynomial.aeval x).toRingHom = ⊥
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>AlgebraicIndependent R x ↔ ∀ (p : MvPolynomial ι R), (MvPolynomial.aeval x) p = 0 → p = 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>h : AlgebraicIndependent R x<VAR>p : MvPolynomial ι R<GOAL>(MvPolynomial.aeval x) p = 0 → p = 0
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>AlgebraicIndependent R x ↔ Function.Injective ⇑(MvPolynomial.aeval x)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>IsEmpty ι<GOAL>AlgebraicIndependent R x ↔ Function.Injective ⇑(algebraMap R A)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<GOAL>Function.Injective ⇑(algebraMap R A)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<GOAL>LinearIndependent R x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>Nontrivial R<GOAL>Function.Injective x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>Nontrivial R<VAR>i : ι<GOAL>x i ≠ 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>f : ι' → ι<VAR>hf : Function.Injective f<GOAL>AlgebraicIndependent R (x ∘ f)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<GOAL>AlgebraicIndependent R Subtype.val
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>CommRing A'<VAR>Algebra R A<VAR>Algebra R A'<VAR>hx : AlgebraicIndependent R x<VAR>f : A →ₐ[R] A'<VAR>hf_inj : Set.InjOn ⇑f ↑(Algebra.adjoin R (Set.range x))<GOAL>AlgebraicIndependent R (⇑f ∘ x)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>CommRing A'<VAR>Algebra R A<VAR>Algebra R A'<VAR>hx : AlgebraicIndependent R x<VAR>f : A →ₐ[R] A'<VAR>hf_inj : Function.Injective ⇑f<GOAL>AlgebraicIndependent R (⇑f ∘ x)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>CommRing A'<VAR>Algebra R A<VAR>Algebra R A'<VAR>f : A →ₐ[R] A'<VAR>hfv : AlgebraicIndependent R (⇑f ∘ x)<GOAL>AlgebraicIndependent R x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>CommRing A'<VAR>Algebra R A<VAR>Algebra R A'<VAR>f : A →ₐ[R] A'<VAR>hf : Function.Injective ⇑f<GOAL>AlgebraicIndependent R (⇑f ∘ x) ↔ AlgebraicIndependent R x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>Subsingleton R<GOAL>AlgebraicIndependent R x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>e : ι ≃ ι'<VAR>f : ι' → A<GOAL>AlgebraicIndependent R (f ∘ ⇑e) ↔ AlgebraicIndependent R f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>e : ι ≃ ι'<VAR>f : ι' → A<VAR>g : ι → A<VAR>h : f ∘ ⇑e = g<GOAL>AlgebraicIndependent R g ↔ AlgebraicIndependent R f
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>ι : Type u_9<VAR>f : ι → A<VAR>hf : Function.Injective f<GOAL>AlgebraicIndependent R Subtype.val ↔ AlgebraicIndependent R f
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>ι : Type u_9<VAR>s : Set ι<VAR>f : ι → A<VAR>hf : Set.InjOn f s<GOAL>(AlgebraicIndependent R fun x => f ↑x) ↔ AlgebraicIndependent R fun x => ↑x
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hs : AlgebraicIndependent R x<GOAL>AlgebraicIndependent R fun i => ⟨x i, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>K : Type u_9<VAR>CommRing K<VAR>Algebra R K<VAR>Algebra K A<VAR>IsScalarTower R K A<VAR>hinj : Function.Injective ⇑(algebraMap R K)<VAR>ai : AlgebraicIndependent K x<GOAL>AlgebraicIndependent R x
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Set A<VAR>li : AlgebraicIndependent R Subtype.val<VAR>t : Finset ↑s<GOAL>AlgebraicIndependent R Subtype.val
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>n : ℕ<VAR>H : ∀ (s : Finset A), (AlgebraicIndependent R fun i => ↑i) → s.card ≤ n<VAR>s : Set A<GOAL>AlgebraicIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Set ι<VAR>hs : AlgebraicIndependent R (x ∘ Subtype.val)<GOAL>AlgebraicIndependent R (s.restrict x)
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>AlgebraicIndependent R Subtype.val ↔ Function.Injective ⇑(algebraMap R A)
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>t s : Set A<VAR>h : t ⊆ s<VAR>hx : AlgebraicIndependent R Subtype.val<GOAL>AlgebraicIndependent R Subtype.val
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>ι : Type u_9<VAR>f : ι → A<VAR>hf : AlgebraicIndependent R f<GOAL>AlgebraicIndependent R Subtype.val
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>ι : Type u_9<VAR>f : ι → A<VAR>hf : AlgebraicIndependent R f<VAR>t : Set A<VAR>ht : Set.range f = t<GOAL>AlgebraicIndependent R Subtype.val
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Set ι<GOAL>AlgebraicIndependent R (x ∘ Subtype.val) ↔ ∀ p ∈ MvPolynomial.supported R s, (MvPolynomial.aeval x) p = 0 → p = 0
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Set A<GOAL>AlgebraicIndependent R Subtype.val ↔ ∀ p ∈ MvPolynomial.supported R s, (MvPolynomial.aeval id) p = 0 → p = 0
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Set A<VAR>H : ∀ t ⊆ s, t.Finite → AlgebraicIndependent R Subtype.val<GOAL>AlgebraicIndependent R Subtype.val
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>ι : Type u_9<VAR>ι' : Type u_10<VAR>s : Set ι<VAR>f : ι → ι'<VAR>g : ι' → A<VAR>hs : AlgebraicIndependent R fun x => g (f ↑x)<GOAL>AlgebraicIndependent R fun x => g ↑x
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>ι : Type u_9<VAR>s : Set ι<VAR>f : ι → A<VAR>hs : AlgebraicIndependent R fun x => f ↑x<GOAL>AlgebraicIndependent R fun x => ↑x
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>η : Type u_9<VAR>Nonempty η<VAR>s : η → Set A<VAR>hs : Directed (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ (i : η), AlgebraicIndependent R Subtype.val<GOAL>AlgebraicIndependent R Subtype.val
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s : Set (Set A)<VAR>hsn : s.Nonempty<VAR>hs : DirectedOn (fun x x_1 => x ⊆ x_1) s<VAR>h : ∀ a ∈ s, AlgebraicIndependent R Subtype.val<GOAL>AlgebraicIndependent R Subtype.val
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>s t : Set A<VAR>hst : s ⊆ t<VAR>hs : AlgebraicIndependent R Subtype.val<GOAL>∃ u, AlgebraicIndependent R Subtype.val ∧ s ⊆ u ∧ u ⊆ t ∧ ∀ (x : Set A), AlgebraicIndependent R Subtype.val → u ⊆ x → x ⊆ t → x = u
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>a : MvPolynomial ι R<GOAL>↑(hx.aevalEquiv a) = (MvPolynomial.aeval x) a
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>b : ↥(Algebra.adjoin R (Set.range x))<GOAL>hx.aevalEquiv.symm b = Function.surjInv ⋯ b
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>p : MvPolynomial ι R<GOAL>(algebraMap (↥(Algebra.adjoin R (Set.range x))) A) (hx.aevalEquiv p) = (MvPolynomial.aeval x) p
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>p : ↥(Algebra.adjoin R (Set.range x))<GOAL>(MvPolynomial.aeval x) (hx.repr p) = ↑p
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<GOAL>(MvPolynomial.aeval x).comp hx.repr = (Algebra.adjoin R (Set.range x)).val
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<GOAL>RingHom.ker ↑hx.repr = ⊥
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>y : MvPolynomial (Option ι) R<GOAL>hx.mvPolynomialOptionEquivPolynomialAdjoin y = Polynomial.map (↑hx.aevalEquiv) ((MvPolynomial.aeval fun o => o.elim Polynomial.X fun s => Polynomial.C (MvPolynomial.X s)) y)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>r : R<GOAL>hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.C r) = Polynomial.C ((algebraMap R ↥(Algebra.adjoin R (Set.range x))) r)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<GOAL>hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X none) = Polynomial.X
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>i : ι<GOAL>hx.mvPolynomialOptionEquivPolynomialAdjoin (MvPolynomial.X (some i)) = Polynomial.C (hx.aevalEquiv (MvPolynomial.X i))
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>a : A<GOAL>(↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom = ↑(MvPolynomial.aeval fun o => o.elim a x)
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hx : AlgebraicIndependent R x<VAR>a : A<GOAL>(AlgebraicIndependent R fun o => o.elim a x) ↔ ¬IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) a
<VAR>R : Type u_3<VAR>A : Type u_5<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>h : Function.Injective ⇑(algebraMap R A)<GOAL>∃ s, IsTranscendenceBasis R Subtype.val
<VAR>ι : Type w<VAR>R : Type u<VAR>CommRing R<VAR>Nontrivial R<VAR>A : Type v<VAR>CommRing A<VAR>Algebra R A<VAR>x : ι → A<VAR>i : AlgebraicIndependent R x<GOAL>IsTranscendenceBasis R x ↔ ∀ (κ : Type v) (w : κ → A), AlgebraicIndependent R w → ∀ (j : ι → κ), w ∘ j = x → Function.Surjective j
<VAR>ι : Type u_1<VAR>R : Type u_3<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>Nontrivial R<VAR>hx : IsTranscendenceBasis R x<GOAL>Algebra.IsAlgebraic (↥(Algebra.adjoin R (Set.range x))) A
<VAR>ι : Type u_1<VAR>K : Type u_4<VAR>A : Type u_5<VAR>x : ι → A<VAR>CommRing A<VAR>Field K<VAR>Algebra K A<VAR>IsEmpty ι<VAR>Nontrivial A<GOAL>AlgebraicIndependent K x
<VAR>K : Type u_4<VAR>A : Type u_5<VAR>CommRing A<VAR>Field K<VAR>Algebra K A<VAR>Nontrivial A<GOAL>AlgebraicIndependent K Subtype.val
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>S : Type v<VAR>NonAssocSemiring S<VAR>f g : R ⧸ I →+* S<VAR>h : f.comp (Ideal.Quotient.mk I) = g.comp (Ideal.Quotient.mk I)<GOAL>f = g
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>x y : R<GOAL>(Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y ↔ x - y ∈ I
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>x : R<GOAL>Submodule.Quotient.mk x = (Ideal.Quotient.mk I) x
<VAR>R : Type u<VAR>CommRing R<VAR>a : R<VAR>I : Ideal R<GOAL>(Ideal.Quotient.mk I) a = 0 ↔ a ∈ I
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<GOAL>(Ideal.Quotient.mk (Ideal.span {x})) y = 0 ↔ x ∣ y
<VAR>R : Type u<VAR>CommRing R<VAR>x : R<GOAL>(Ideal.Quotient.mk (Ideal.span {x})) x = 0
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>0 = 1 ↔ I = ⊤
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>0 ≠ 1 ↔ I ≠ ⊤
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>hI : I ≠ ⊤<GOAL>Nontrivial (R ⧸ I)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>Subsingleton (R ⧸ I) ↔ I = ⊤
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>Function.Surjective ⇑(Ideal.Quotient.mk I)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>s : Set R<GOAL>⇑(Ideal.Quotient.mk I) ⁻¹' (⇑(Ideal.Quotient.mk I) '' s) = ⋃ x, (fun y => ↑x + y) '' s
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>IsDomain (R ⧸ I) ↔ I.IsPrime
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>hI : I.IsMaximal<VAR>a : R ⧸ I<GOAL>a ≠ 0 → ∃ b, a * b = 1
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>hqf : IsField (R ⧸ I)<GOAL>I.IsMaximal
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I.IsMaximal ↔ IsField (R ⧸ I)
<VAR>R : Type u<VAR>CommRing R<VAR>a : R<VAR>S : Type v<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<GOAL>(Ideal.Quotient.lift I f H) ((Ideal.Quotient.mk I) a) = f a
<VAR>R : Type u<VAR>CommRing R<VAR>S : Type v<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective ⇑(Ideal.Quotient.lift I f H)
<VAR>R : Type u<VAR>CommRing R<VAR>S T : Ideal R<VAR>H : S ≤ T<VAR>x : R<GOAL>(Ideal.Quotient.factor S T H) ((Ideal.Quotient.mk S) x) = (Ideal.Quotient.mk T) x
<VAR>R : Type u<VAR>CommRing R<VAR>S T : Ideal R<VAR>H : S ≤ T<GOAL>(Ideal.Quotient.factor S T H).comp (Ideal.Quotient.mk S) = Ideal.Quotient.mk T
<VAR>R : Type u_1<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : I = J<VAR>x : R<GOAL>(Ideal.quotEquivOfEq h) ((Ideal.Quotient.mk I) x) = (Ideal.Quotient.mk J) x
<VAR>R : Type u_1<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : I = J<GOAL>(Ideal.quotEquivOfEq h).symm = Ideal.quotEquivOfEq ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>ι : Type u_1<VAR>Finite ι<VAR>ι' : Type w<VAR>x : ι → R<VAR>hi : ∀ (i : ι), x i ∈ I<VAR>f : (ι → R) →ₗ[R] ι' → R<VAR>i : ι'<GOAL>f x i ∈ I
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u<VAR>Fintype ι<VAR>f : ι → R<VAR>x : ι → M<GOAL>Module.IsTrivialRelation f x ↔ TensorProduct.VanishesTrivially R f x
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>ι : Type u<VAR>Fintype ι<VAR>f : ι → R<VAR>x : ι → M<VAR>h : Module.IsTrivialRelation f x<GOAL>∑ i : ι, f i • x i = 0
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>[Module.Flat R M, ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I)), ∀ {ι : Type u} [inst : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i : ι, f i ⊗ₜ[R] x i = 0 → TensorProduct.VanishesTrivially R f x, ∀ {ι : Type u} [inst : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i : ι, f i • x i = 0 → Module.IsTrivialRelation f x, ∀ {ι : Type u} [inst : Fintype ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M}, x f = 0 → ∃ κ x_1 a y, x = y ∘ₗ a ∧ a f = 0, ∀ {N : Type u} [inst : AddCommGroup N] [inst_1 : Module R N] [inst_2 : Module.Free R N] [inst_3 : Module.Finite R N] {f : N} {x : N →ₗ[R] M}, x f = 0 → ∃ κ x_1 a y, x = y ∘ₗ a ∧ a f = 0].TFAE
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Flat R M ↔ ∀ {ι : Type u} [inst : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i : ι, f i • x i = 0 → Module.IsTrivialRelation f x
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Flat R M<VAR>ι : Type u<VAR>Fintype ι<VAR>f : ι → R<VAR>x : ι → M<VAR>h : ∑ i : ι, f i • x i = 0<GOAL>Module.IsTrivialRelation f x
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>hfx : ∀ {ι : Type u} [inst : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i : ι, f i • x i = 0 → Module.IsTrivialRelation f x<GOAL>Module.Flat R M
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>Module.Flat R M ↔ ∀ {ι : Type u} [inst : Fintype ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M}, x f = 0 → ∃ κ x_1 a y, x = y ∘ₗ a ∧ a f = 0
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Flat R M<VAR>ι : Type u<VAR>Finite ι<VAR>f : ι →₀ R<VAR>x : (ι →₀ R) →ₗ[R] M<VAR>h : x f = 0<GOAL>∃ κ x_1 a y, x = y ∘ₗ a ∧ a f = 0
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>h : ∀ {ι : Type u} [inst : Fintype ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M}, x f = 0 → ∃ κ x_1 a y, x = y ∘ₗ a ∧ a f = 0<GOAL>Module.Flat R M
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Flat R M<VAR>N : Type u<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R N<VAR>Module.Finite R N<VAR>f : N<VAR>x : N →ₗ[R] M<VAR>h : x f = 0<GOAL>∃ κ x_1 a y, x = y ∘ₗ a ∧ a f = 0
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Flat R M<VAR>K N : Type u<VAR>AddCommGroup K<VAR>Module R K<VAR>Module.Finite R K<VAR>AddCommGroup N<VAR>Module R N<VAR>Module.Free R N<VAR>Module.Finite R N<VAR>f : K →ₗ[R] N<VAR>x : N →ₗ[R] M<VAR>h : x ∘ₗ f = 0<GOAL>∃ κ x_1 a y, x = y ∘ₗ a ∧ a ∘ₗ f = 0
<VAR>R M : Type u<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Flat R M<VAR>P : Type u<VAR>AddCommGroup P<VAR>Module R P<VAR>Module.FinitePresentation R P<VAR>h₁ : P →ₗ[R] M<GOAL>∃ κ x h₂ h₃, h₁ = h₃ ∘ₗ h₂
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddCommMonoid X<VAR>Module R X<VAR>x : OreLocalization S X<GOAL>0 • x = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddCommMonoid X<VAR>Module R X<VAR>y z : OreLocalization S R<VAR>x : OreLocalization S X<GOAL>(y + z) • x = y • x + z • x
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>x : OreLocalization S R<GOAL>0 * x = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>x : OreLocalization S R<GOAL>x * 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>x y z : OreLocalization S R<GOAL>x * (y + z) = x * y + x * z
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>x y z : OreLocalization S R<GOAL>(x + y) * z = x * z + y * z
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddCommMonoid X<VAR>Module R X<VAR>n : ℕ<VAR>x : OreLocalization S X<GOAL>n • x = n • x
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>r : R<GOAL>OreLocalization.numeratorRingHom r = r /ₒ 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>T : Type u_3<VAR>Semiring T<VAR>f : R →+* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>r : R<VAR>s : ↥S<GOAL>(OreLocalization.universalHom f fS hf) (r /ₒ s) = ↑(fS s)⁻¹ * f r
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>T : Type u_3<VAR>Semiring T<VAR>f : R →+* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>r : R<GOAL>(OreLocalization.universalHom f fS hf) (OreLocalization.numeratorHom r) = f r
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>T : Type u_3<VAR>Semiring T<VAR>f : R →+* T<VAR>fS : ↥S →* Tˣ<VAR>hf : ∀ (s : ↥S), f ↑s = ↑(fS s)<VAR>φ : OreLocalization S R →+* T<VAR>huniv : ∀ (r : R), φ (OreLocalization.numeratorHom r) = f r<GOAL>φ = OreLocalization.universalHom f fS hf
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>X : Type u_2<VAR>AddCommGroup X<VAR>Module R X<VAR>n : ℤ<VAR>x : OreLocalization S X<GOAL>n • x = n • x
<VAR>R : Type u_1<VAR>Ring R<VAR>S : Submonoid R<VAR>OreLocalization.OreSet S<VAR>hS : S ≤ nonZeroDivisorsRight R<GOAL>Function.Injective ⇑OreLocalization.numeratorHom