ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.restrictScalars S (KaehlerDifferential.ideal R S)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = KaehlerDifferential.ideal R S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>s : S<GOAL>(KaehlerDifferential.DLinearMap R S) s = (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, ⋯⟩
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>s : S<GOAL>(KaehlerDifferential.D R S) s = (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, ⋯⟩
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>h : Function.Surjective ⇑(algebraMap R S)<GOAL>Subsingleton (Ω[S⁄R])
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>D : Derivation R S M<VAR>x : ↥(KaehlerDifferential.ideal R S)<GOAL>D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent x) = D.tensorProductTo ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>D : Derivation R S M<GOAL>D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>D' : Derivation R S M<VAR>x : S<GOAL>D'.liftKaehlerDifferential ((KaehlerDifferential.D R S) x) = D' x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>f f' : Ω[S⁄R] →ₗ[S] M<VAR>hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)<GOAL>f = f'
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>(KaehlerDifferential.D R S).liftKaehlerDifferential = LinearMap.id
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : ↥(KaehlerDifferential.ideal R S)<GOAL>(KaehlerDifferential.D R S).tensorProductTo ↑x = (KaehlerDifferential.ideal R S).toCotangent x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>Function.Surjective ⇑(KaehlerDifferential.D R S).tensorProductTo
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>D : Derivation R S M<GOAL>(KaehlerDifferential.linearMapEquivDerivation R S).symm D = D.liftKaehlerDifferential
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>M : Type u_1<VAR>AddCommGroup M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>m : Ω[S⁄R] →ₗ[S] M<GOAL>∀ (a : S), ((KaehlerDifferential.linearMapEquivDerivation R S) m) a = m ((KaehlerDifferential.D R S) a)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>f : S →ₐ[R] TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2<GOAL>(Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f = IsScalarTower.toAlgHom R S ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ (KaehlerDifferential.ideal R S).cotangentIdeal) ↔ (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>Algebra.EssFiniteType R S<GOAL>(KaehlerDifferential.ideal R S).FG
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x y z : S<GOAL>(KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single (x + y) z) = (KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single x z) + (KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single y z)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x y z : S<GOAL>(KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single (x * y) z) = (KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single y (z * x)) + (KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single x (z * y))
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : R<VAR>y : S<GOAL>(KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single ((algebraMap R S) x) y) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>(KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single 1 x) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>x y : S<GOAL>(KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single (r • x) y) = r • (KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single x y)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>x : S<GOAL>(KaehlerDifferential.derivationQuotKerTotal R S) x = (KaehlerDifferential.kerTotal R S).mkQ (Finsupp.single x 1)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>(KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ Finsupp.total S (Ω[S⁄R]) S ⇑(KaehlerDifferential.D R S) = (KaehlerDifferential.kerTotal R S).mkQ
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>LinearMap.ker (Finsupp.total S (Ω[S⁄R]) S ⇑(KaehlerDifferential.D R S)) = KaehlerDifferential.kerTotal R S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>Function.Surjective ⇑(Finsupp.total S (Ω[S⁄R]) S ⇑(KaehlerDifferential.D R S))
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>a : Ω[S⁄R]<GOAL>(KaehlerDifferential.quotKerTotalEquiv R S).symm a = (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>∀ (a : (S →₀ S) ⧸ (KaehlerDifferential.kerTotal R S).toAddSubgroup), (KaehlerDifferential.quotKerTotalEquiv R S) a = (QuotientAddGroup.lift (KaehlerDifferential.kerTotal R S).toAddSubgroup (Finsupp.total S (Ω[S⁄R]) S ⇑(KaehlerDifferential.D R S)).toAddMonoidHom ⋯) a
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<GOAL>(↑(KaehlerDifferential.quotKerTotalEquiv R S).symm).compDer (KaehlerDifferential.D R S) = KaehlerDifferential.derivationQuotKerTotal R S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>Algebra S B<VAR>IsScalarTower R A B<VAR>IsScalarTower R S B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (KaehlerDifferential.kerTotal R A) ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap S B) x) 1) = Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B)
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (KaehlerDifferential.kerTotal R A ⊔ Submodule.span A (Set.range fun x => Finsupp.single ((algebraMap R A) x) 1)) = Submodule.restrictScalars A (KaehlerDifferential.kerTotal R B)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>Algebra S B<VAR>IsScalarTower R A B<VAR>IsScalarTower R S B<VAR>SMulCommClass S A B<GOAL>(KaehlerDifferential.map R S A B).compDer (KaehlerDifferential.D R A) = Derivation.compAlgebraMap A (Derivation.restrictScalars R (KaehlerDifferential.D S B))
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>Algebra S B<VAR>IsScalarTower R A B<VAR>IsScalarTower R S B<VAR>SMulCommClass S A B<VAR>x : A<GOAL>(KaehlerDifferential.map R S A B) ((KaehlerDifferential.D R A) x) = (KaehlerDifferential.D S B) ((algebraMap A B) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>Algebra S B<VAR>IsScalarTower R A B<VAR>IsScalarTower R S B<VAR>SMulCommClass S A B<GOAL>LinearMap.ker (KaehlerDifferential.map R S A B) = Submodule.map (Finsupp.total A (Ω[A⁄R]) A ⇑(KaehlerDifferential.D R A)) (Submodule.comap (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B)))
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>LinearMap.ker (KaehlerDifferential.map R R A B) = Submodule.map (Finsupp.total A (Ω[A⁄R]) A ⇑(KaehlerDifferential.D R A)) (LinearMap.ker (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)))
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>Algebra S B<VAR>IsScalarTower R A B<VAR>IsScalarTower R S B<VAR>SMulCommClass S A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Function.Surjective ⇑(KaehlerDifferential.map R S A B)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra S B<VAR>IsScalarTower R S B<GOAL>Function.Surjective ⇑(KaehlerDifferential.map R S B B)
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>x : B<VAR>y : Ω[A⁄R]<GOAL>(KaehlerDifferential.mapBaseChange R A B) (x ⊗ₜ[A] y) = x • (KaehlerDifferential.map R R A B) y
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<GOAL>LinearMap.range (KaehlerDifferential.mapBaseChange R A B) = LinearMap.ker (KaehlerDifferential.map R A B B)
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<GOAL>Function.Exact ⇑(KaehlerDifferential.mapBaseChange R A B) ⇑(KaehlerDifferential.map R A B B)
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra A B<VAR>x : ↥(RingHom.ker (algebraMap A B))<GOAL>(KaehlerDifferential.kerToTensor R A B) x = 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra A B<VAR>x : ↥(RingHom.ker (algebraMap A B))<GOAL>(KaehlerDifferential.kerCotangentToTensor R A B) ((RingHom.ker (algebraMap A B)).toCotangent x) = 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>LinearMap.range (KaehlerDifferential.kerCotangentToTensor R A B) = Submodule.restrictScalars A (LinearMap.ker (KaehlerDifferential.mapBaseChange R A B))
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B)
<VAR>R : Type u<VAR>CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommRing A<VAR>CommRing B<VAR>Algebra R A<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>h : Function.Surjective ⇑(algebraMap A B)<GOAL>Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>self : Algebra.Flat R S<GOAL>Module.Flat R S
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>T : Type w<VAR>CommRing T<VAR>Algebra R S<VAR>Algebra R T<VAR>Algebra S T<VAR>IsScalarTower R S T<VAR>Algebra.Flat R S<VAR>Algebra.Flat S T<GOAL>Algebra.Flat R T
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>R' : Type w<VAR>S' : Type t<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R' S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>h : Algebra.IsPushout R S R' S'<VAR>Algebra.Flat R R'<GOAL>Algebra.Flat S S'
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>self : f.Flat<GOAL>Algebra.Flat R S
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>Module.Flat R ↑M<VAR>C : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hC : C.Exact<GOAL>(C.map (CategoryTheory.MonoidalCategory.tensorLeft M)).Exact
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>Module.Flat R ↑M<VAR>C : CategoryTheory.ShortComplex (ModuleCat R)<VAR>hC : C.Exact<GOAL>(C.map (CategoryTheory.MonoidalCategory.tensorRight M)).Exact
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<GOAL>Module.Flat R ↑M ↔ ∀ (C : CategoryTheory.ShortComplex (ModuleCat R)), C.Exact → (C.map (CategoryTheory.MonoidalCategory.tensorLeft M)).Exact
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<GOAL>Module.Flat R ↑M ↔ ∀ (C : CategoryTheory.ShortComplex (ModuleCat R)), C.Exact → (C.map (CategoryTheory.MonoidalCategory.tensorRight M)).Exact
<VAR>R : Type u<VAR>Ring R<VAR>self : IsBezout R<VAR>I : Ideal R<GOAL>I.FG → Submodule.IsPrincipal I
<VAR>R : Type u<VAR>M : Type v<VAR>AddCommGroup M<VAR>Ring R<VAR>Module R M<VAR>S : Submodule R M<VAR>S.IsPrincipal<GOAL>Submodule.span R {Submodule.IsPrincipal.generator S} = S
<VAR>R : Type u<VAR>Ring R<VAR>I : Ideal R<VAR>Submodule.IsPrincipal I<GOAL>Ideal.span {Submodule.IsPrincipal.generator I} = I
<VAR>R : Type u<VAR>M : Type v<VAR>AddCommGroup M<VAR>Ring R<VAR>Module R M<VAR>S : Submodule R M<VAR>S.IsPrincipal<GOAL>Submodule.IsPrincipal.generator S ∈ S
<VAR>R : Type u<VAR>M : Type v<VAR>AddCommGroup M<VAR>Ring R<VAR>Module R M<VAR>S : Submodule R M<VAR>S.IsPrincipal<VAR>x : M<GOAL>x ∈ S ↔ ∃ s, x = s • Submodule.IsPrincipal.generator S
<VAR>R : Type u<VAR>M : Type v<VAR>AddCommGroup M<VAR>Ring R<VAR>Module R M<VAR>S : Submodule R M<VAR>S.IsPrincipal<GOAL>S = ⊥ ↔ Submodule.IsPrincipal.generator S = 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsPrincipalIdealRing R<VAR>IsDomain R<VAR>r : R<GOAL>Associated (Submodule.IsPrincipal.generator (Ideal.span {r})) r
<VAR>R : Type u<VAR>CommRing R<VAR>S : Ideal R<VAR>Submodule.IsPrincipal S<VAR>x : R<GOAL>x ∈ S ↔ Submodule.IsPrincipal.generator S ∣ x
<VAR>R : Type u<VAR>CommRing R<VAR>S : Ideal R<VAR>Submodule.IsPrincipal S<VAR>is_prime : S.IsPrime<VAR>ne_bot : S ≠ ⊥<GOAL>Prime (Submodule.IsPrincipal.generator S)
<VAR>R : Type u<VAR>M : Type v<VAR>AddCommGroup M<VAR>CommRing R<VAR>Module R M<VAR>N : Submodule R M<VAR>ϕ : M →ₗ[R] R<VAR>(Submodule.map ϕ N).IsPrincipal<VAR>x : M<VAR>hx : x ∈ N<GOAL>Submodule.IsPrincipal.generator (Submodule.map ϕ N) ∣ ϕ x
<VAR>R : Type u<VAR>M : Type v<VAR>AddCommGroup M<VAR>CommRing R<VAR>Module R M<VAR>N O : Submodule R M<VAR>hNO : N ≤ O<VAR>ϕ : ↥O →ₗ[R] R<VAR>(ϕ.submoduleImage N).IsPrincipal<VAR>x : M<VAR>hx : x ∈ N<GOAL>Submodule.IsPrincipal.generator (ϕ.submoduleImage N) ∣ ϕ ⟨x, ⋯⟩
<VAR>R : Type u<VAR>Ring R<VAR>x y : R<VAR>Submodule.IsPrincipal (Ideal.span {x, y})<GOAL>Ideal.span {IsBezout.gcd x y} = Ideal.span {x, y}
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>Submodule.IsPrincipal (Ideal.span {x, y})<GOAL>IsBezout.gcd x y ∣ x
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>Submodule.IsPrincipal (Ideal.span {x, y})<GOAL>IsBezout.gcd x y ∣ y
<VAR>R : Type u<VAR>CommRing R<VAR>x y z : R<VAR>Submodule.IsPrincipal (Ideal.span {x, y})<VAR>hx : z ∣ x<VAR>hy : z ∣ y<GOAL>z ∣ IsBezout.gcd x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>Submodule.IsPrincipal (Ideal.span {x, y})<GOAL>∃ a b, a * x + b * y = IsBezout.gcd x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>Submodule.IsPrincipal (Ideal.span {x, y})<VAR>h : IsRelPrime x y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>Submodule.IsPrincipal (Ideal.span {x, y})<GOAL>IsRelPrime x y ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>x y : R<VAR>Submodule.IsPrincipal (Ideal.span {x, y})<VAR>IsDomain R<VAR>GCDMonoid R<GOAL>Associated (IsBezout.gcd x y) (gcd x y)
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>S : Ideal R<VAR>hpi : S.IsPrime<VAR>hS : S ≠ ⊥<GOAL>S.IsMaximal
<VAR>R : Type u<VAR>EuclideanDomain R<VAR>S : Ideal R<VAR>x y : R<VAR>hy : y ∈ S<GOAL>x % y ∈ S ↔ x ∈ S
<VAR>R : Type u_1<VAR>CommRing R<VAR>h : IsField R<GOAL>IsPrincipalIdealRing R
<VAR>R : Type u<VAR>CommRing R<VAR>IsPrincipalIdealRing R<VAR>p : R<VAR>hp : Irreducible p<GOAL>Ideal.IsMaximal (Submodule.span R {p})
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>a : R<VAR>h : a ≠ 0<GOAL>(∀ b ∈ PrincipalIdealRing.factors a, Irreducible b) ∧ Associated (PrincipalIdealRing.factors a).prod a
<VAR>R : Type v<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>a b : R<VAR>ha : a ≠ 0<VAR>hb : b ∈ PrincipalIdealRing.factors a<GOAL>b ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>s : Submonoid R<VAR>a : R<VAR>ha : a ≠ 0<VAR>hfac : ∀ b ∈ PrincipalIdealRing.factors a, b ∈ s<VAR>hunit : ∀ (c : Rˣ), ↑c ∈ s<GOAL>a ∈ s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>Semiring S<VAR>f : R →+* S<VAR>s : Submonoid S<VAR>a : R<VAR>ha : a ≠ 0<VAR>h : ∀ b ∈ PrincipalIdealRing.factors a, f b ∈ s<VAR>hf : ∀ (c : Rˣ), f ↑c ∈ s<GOAL>f a ∈ s
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type u_2<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup N<VAR>Module R M<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<VAR>S : Submodule R N<VAR>hI : (Submodule.comap f S).IsPrincipal<GOAL>S.IsPrincipal
<VAR>R : Type u<VAR>S : Type u_1<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal S<VAR>hI : Submodule.IsPrincipal (Ideal.comap f I)<GOAL>Submodule.IsPrincipal I
<VAR>R : Type u<VAR>S : Type u_1<VAR>Ring R<VAR>Ring S<VAR>IsPrincipalIdealRing R<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>IsPrincipalIdealRing S
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsBezout R<VAR>GCDMonoid R<VAR>x y : R<GOAL>Ideal.span {gcd x y} = Ideal.span {IsBezout.gcd x y}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsBezout R<VAR>GCDMonoid R<VAR>x y : R<GOAL>Ideal.span {gcd x y} = Ideal.span {x, y}
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsBezout R<VAR>GCDMonoid R<VAR>a b : R<VAR>z : R<GOAL>gcd a b ∣ z ↔ ∃ x y, z = a * x + b * y
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsBezout R<VAR>GCDMonoid R<VAR>a b : R<GOAL>∃ x y, gcd a b = a * x + b * y
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsBezout R<VAR>GCDMonoid R<VAR>x y : R<GOAL>IsUnit (gcd x y) ↔ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>IsBezout R<VAR>x y : R<VAR>nonzero : ¬(x = 0 ∧ y = 0)<VAR>H : ∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬z ∣ y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>IsBezout R<VAR>x y : R<VAR>h : Irreducible x<GOAL>x ∣ y ∨ IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>IsBezout R<VAR>p n : R<VAR>hp : Irreducible p<GOAL>IsCoprime p n ↔ ¬p ∣ n
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsBezout R<VAR>p n : R<VAR>hp : Prime p<GOAL>IsCoprime p n ↔ ¬p ∣ n
<VAR>R : Type u<VAR>CommRing R<VAR>IsBezout R<VAR>p n : R<VAR>hp : Irreducible p<GOAL>p ∣ n ↔ ¬IsCoprime p n
<VAR>R : Type u<VAR>CommRing R<VAR>IsBezout R<VAR>p a : R<VAR>m : ℕ<VAR>hp : Irreducible p<VAR>h : ¬p ∣ a<GOAL>IsCoprime a (p ^ m)
<VAR>R : Type u<VAR>CommRing R<VAR>IsBezout R<VAR>p : R<VAR>hp : Irreducible p<VAR>i : R<GOAL>IsCoprime p i ∨ p ∣ i
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsBezout R<VAR>a b c : R<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>h : a * b = c ^ k<GOAL>∃ d, Associated (d ^ k) a
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsBezout R<VAR>a b c : R<VAR>hab : IsCoprime a b<VAR>k : ℕ<VAR>h : Associated (c ^ k) (a * b)<GOAL>∃ d, Associated (d ^ k) a
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>x y : R<VAR>nonzero : ¬(x = 0 ∧ y = 0)<VAR>H : ∀ (z : R), Irreducible z → z ∣ x → ¬z ∣ y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>x y : R<VAR>nonzero : ¬(x = 0 ∧ y = 0)<VAR>H : ∀ (z : R), Prime z → z ∣ x → ¬z ∣ y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>I ∈ nonPrincipals R ↔ ¬Submodule.IsPrincipal I
<VAR>R : Type u<VAR>CommRing R<GOAL>nonPrincipals R = ∅ ↔ IsPrincipalIdealRing R
<VAR>R : Type u<VAR>CommRing R<VAR>c : Set (Ideal R)<VAR>hs : c ⊆ nonPrincipals R<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<GOAL>∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I
<VAR>R : Type u<VAR>CommRing R<VAR>H : ∀ (P : Ideal R), P.IsPrime → Submodule.IsPrincipal P<GOAL>IsPrincipalIdealRing R
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>f ∈ reesAlgebra I ↔ ∀ (i : ℕ), f.coeff i ∈ I ^ i
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>f : R[X]<GOAL>f ∈ reesAlgebra I ↔ ∀ i ∈ f.support, f.coeff i ∈ I ^ i
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>i : ℕ<VAR>r : R<GOAL>(Polynomial.monomial i) r ∈ reesAlgebra I ↔ r ∈ I ^ i
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>n : ℕ<VAR>r : R<VAR>hr : r ∈ I ^ n<GOAL>(Polynomial.monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>Algebra.adjoin R ↑(Submodule.map (Polynomial.monomial 1) I) = reesAlgebra I
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>hI : I.FG<GOAL>(reesAlgebra I).FG
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>multiplicity.Finite a b ↔ (multiplicity a b).Dom
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<GOAL>multiplicity.Finite a b ↔ ∃ n, ¬a ^ (n + 1) ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a : α<GOAL>multiplicity.Finite a 1 → ¬a ∣ 1
<VAR>a b : ℕ<GOAL>multiplicity ↑a ↑b = multiplicity a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<GOAL>¬multiplicity.Finite a b ↔ ∀ (n : ℕ), a ^ n ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b : α<VAR>h : multiplicity.Finite a b<GOAL>¬IsUnit a
<VAR>α : Type u_1<VAR>Monoid α<VAR>a b c : α<GOAL>multiplicity.Finite a (b * c) → multiplicity.Finite a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>k : ℕ<GOAL>↑k ≤ multiplicity a b → a ^ k ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>h : multiplicity.Finite a b<GOAL>a ^ (multiplicity a b).get h ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>m : ℕ<VAR>hm : multiplicity a b < ↑m<GOAL>¬a ^ m ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>m : ℕ<VAR>h : multiplicity.Finite a b<VAR>hm : (multiplicity a b).get h < m<GOAL>¬a ^ m ∣ b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>hfin : multiplicity.Finite a b<VAR>hdiv : a ∣ b<GOAL>0 < (multiplicity a b).get hfin
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>k : ℕ<VAR>hk : a ^ k ∣ b<VAR>hsucc : ¬a ^ (k + 1) ∣ b<GOAL>↑k = multiplicity a b
<VAR>α : Type u_1<VAR>Monoid α<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>k : ℕ<VAR>hk : a ^ k ∣ b<VAR>hsucc : ¬a ^ (k + 1) ∣ b<GOAL>k = (multiplicity a b).get ⋯