ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R ≃+* S<VAR>K : NonUnitalSubsemiring R<GOAL>NonUnitalSubsemiring.map (↑f) K = NonUnitalSubsemiring.comap f.symm K
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>f : R ≃+* S<VAR>K : NonUnitalSubsemiring S<GOAL>NonUnitalSubsemiring.comap (↑f) K = NonUnitalSubsemiring.map f.symm K
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<GOAL>↑M.nonUnitalSubsemiringClosure = ↑(AddSubmonoid.closure ↑M)
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<GOAL>M.nonUnitalSubsemiringClosure.toAddSubmonoid = AddSubmonoid.closure ↑M
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<GOAL>M.nonUnitalSubsemiringClosure = NonUnitalSubsemiring.closure ↑M
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<GOAL>NonUnitalSubsemiring.closure ↑(Subsemigroup.closure s) = NonUnitalSubsemiring.closure s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<GOAL>↑(NonUnitalSubsemiring.closure s) = ↑(AddSubmonoid.closure ↑(Subsemigroup.closure s))
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>x : R<GOAL>x ∈ NonUnitalSubsemiring.closure s ↔ x ∈ AddSubmonoid.closure ↑(Subsemigroup.closure s)
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<GOAL>NonUnitalSubsemiring.closure ↑(AddSubmonoid.closure s) = NonUnitalSubsemiring.closure s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>p : R → Prop<VAR>x : R<VAR>h : x ∈ NonUnitalSubsemiring.closure s<VAR>mem : ∀ x ∈ s, p x<VAR>zero : p 0<VAR>add : ∀ (x y : R), p x → p y → p (x + y)<VAR>mul : ∀ (x y : R), p x → p y → p (x * y)<GOAL>p x
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set R<VAR>p : R → R → Prop<VAR>x y : R<VAR>hx : x ∈ NonUnitalSubsemiring.closure s<VAR>hy : y ∈ NonUnitalSubsemiring.closure s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>H0_left : ∀ (x : R), p 0 x<VAR>H0_right : ∀ (x : R), p x 0<VAR>Hadd_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : R), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : R), p x y₁ → p x y₂ → p x (y₁ * y₂)<GOAL>p x y
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<GOAL>NonUnitalSubsemiring.closure ↑s = s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>NonUnitalSubsemiring.closure ∅ = ⊥
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<GOAL>NonUnitalSubsemiring.closure Set.univ = ⊤
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s t : Set R<GOAL>NonUnitalSubsemiring.closure (s ∪ t) = NonUnitalSubsemiring.closure s ⊔ NonUnitalSubsemiring.closure t
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>ι : Sort u_2<VAR>s : ι → Set R<GOAL>NonUnitalSubsemiring.closure (⋃ i, s i) = ⨆ i, NonUnitalSubsemiring.closure (s i)
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : Set (Set R)<GOAL>NonUnitalSubsemiring.closure (⋃₀ s) = ⨆ t ∈ s, NonUnitalSubsemiring.closure t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s t : NonUnitalSubsemiring R<VAR>f : F<GOAL>NonUnitalSubsemiring.map f (s ⊔ t) = NonUnitalSubsemiring.map f s ⊔ NonUnitalSubsemiring.map f t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>ι : Sort u_2<VAR>f : F<VAR>s : ι → NonUnitalSubsemiring R<GOAL>NonUnitalSubsemiring.map f (iSup s) = ⨆ i, NonUnitalSubsemiring.map f (s i)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s t : NonUnitalSubsemiring S<VAR>f : F<GOAL>NonUnitalSubsemiring.comap f (s ⊓ t) = NonUnitalSubsemiring.comap f s ⊓ NonUnitalSubsemiring.comap f t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>ι : Sort u_2<VAR>f : F<VAR>s : ι → NonUnitalSubsemiring S<GOAL>NonUnitalSubsemiring.comap f (iInf s) = ⨅ i, NonUnitalSubsemiring.comap f (s i)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<GOAL>NonUnitalSubsemiring.map f ⊥ = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<GOAL>NonUnitalSubsemiring.comap f ⊤ = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>s : NonUnitalSubsemiring R<VAR>t : NonUnitalSubsemiring S<GOAL>↑(s.prod t) = ↑s ×ˢ ↑t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>s : NonUnitalSubsemiring R<VAR>t : NonUnitalSubsemiring S<VAR>p : R × S<GOAL>p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>s₁ s₂ : NonUnitalSubsemiring R<VAR>hs : s₁ ≤ s₂<VAR>t₁ t₂ : NonUnitalSubsemiring S<VAR>ht : t₁ ≤ t₂<GOAL>s₁.prod t₁ ≤ s₂.prod t₂
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>s : NonUnitalSubsemiring R<GOAL>Monotone fun t => s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>t : NonUnitalSubsemiring S<GOAL>Monotone fun s => s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>s : NonUnitalSubsemiring R<GOAL>s.prod ⊤ = NonUnitalSubsemiring.comap (NonUnitalRingHom.fst R S) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>s : NonUnitalSubsemiring S<GOAL>⊤.prod s = NonUnitalSubsemiring.comap (NonUnitalRingHom.snd R S) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<GOAL>⊤.prod ⊤ = ⊤
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>ι : Sort u_2<VAR>hι : Nonempty ι<VAR>S : ι → NonUnitalSubsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>ι : Sort u_2<VAR>hι : Nonempty ι<VAR>S : ι → NonUnitalSubsemiring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>S : Set (NonUnitalSubsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>S : Set (NonUnitalSubsemiring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<GOAL>↑(sSup S) = ⋃ s ∈ S, ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>x : R<GOAL>↑((NonUnitalRingHom.srangeRestrict f) x) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<GOAL>Function.Surjective ⇑(NonUnitalRingHom.srangeRestrict f)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<GOAL>NonUnitalRingHom.srange f = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>NonUnitalRingHom.srange f = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f g : F<VAR>s : Set R<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(NonUnitalSubsemiring.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>F : Type u_1<VAR>FunLike F R S<VAR>f g : F<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s : Set R<VAR>hs : NonUnitalSubsemiring.closure s = ⊤<VAR>f g : F<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : Set S<GOAL>NonUnitalSubsemiring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubsemiring.comap f (NonUnitalSubsemiring.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : Set R<GOAL>NonUnitalSubsemiring.map f (NonUnitalSubsemiring.closure s) = NonUnitalSubsemiring.closure (⇑f '' s)
<VAR>R : Type u<VAR>NonUnitalNonAssocSemiring R<VAR>s : NonUnitalSubsemiring R<GOAL>NonUnitalRingHom.srange (NonUnitalSubsemiringClass.subtype s) = s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<GOAL>NonUnitalRingHom.srange (NonUnitalRingHom.fst R S) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<GOAL>NonUnitalRingHom.srange (NonUnitalRingHom.snd R S) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>g : S → R<VAR>f : F<VAR>h : Function.LeftInverse g ⇑f<VAR>x : R<GOAL>↑((RingEquiv.sofLeftInverse' h) x) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>F : Type u_1<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>g : S → R<VAR>f : F<VAR>h : Function.LeftInverse g ⇑f<VAR>x : ↥(NonUnitalRingHom.srange f)<GOAL>(RingEquiv.sofLeftInverse' h).symm x = g ↑x
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>e : R ≃+* S<VAR>s : NonUnitalSubsemiring R<VAR>y : ↑(⇑↑e.toAddEquiv '' ↑s.toAddSubmonoid)<GOAL>↑((e.nonUnitalSubsemiringMap s).symm y) = (↑e).symm ↑y
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocSemiring R<VAR>NonUnitalNonAssocSemiring S<VAR>e : R ≃+* S<VAR>s : NonUnitalSubsemiring R<VAR>x : ↑↑s.toAddSubmonoid<GOAL>↑((e.nonUnitalSubsemiringMap s) x) = e ↑x
<VAR>R : Type u_4<VAR>K : Type u_5<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>toPrincipalIdeal R K = { toFun := fun x => { val := FractionalIdeal.spanSingleton R⁰ ↑x, inv := FractionalIdeal.spanSingleton R⁰ (↑x)⁻¹, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : Kˣ<GOAL>↑((toPrincipalIdeal R K) x) = FractionalIdeal.spanSingleton R⁰ ↑x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : (FractionalIdeal R⁰ K)ˣ<VAR>x : Kˣ<GOAL>(toPrincipalIdeal R K) x = I ↔ FractionalIdeal.spanSingleton R⁰ ↑x = ↑I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>I ∈ (toPrincipalIdeal R K).range ↔ ∃ x, FractionalIdeal.spanSingleton R⁰ x = ↑I
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>Quot.mk Setoid.r I = ClassGroup.mk I
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>I J : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>ClassGroup.mk I = ClassGroup.mk J ↔ ∃ x, I * (toPrincipalIdeal R (FractionRing R)) x = J
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>I J : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>I' J' : Ideal R<VAR>hI : ↑I = ↑I'<VAR>hJ : ↑J = ↑J'<GOAL>ClassGroup.mk I = ClassGroup.mk J ↔ ∃ x y, x ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x} * I' = Ideal.span {y} * J'
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<VAR>I' : Ideal R<VAR>hI : ↑I = ↑I'<GOAL>ClassGroup.mk I = 1 ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>P : ClassGroup R → Prop<VAR>h : ∀ (I : (FractionalIdeal R⁰ K)ˣ), P (ClassGroup.mk I)<VAR>x : ClassGroup R<GOAL>P x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>K' : Type u_4<VAR>Field K'<VAR>Algebra R K'<VAR>IsFractionRing R K'<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>(ClassGroup.equiv K') (ClassGroup.mk I) = (QuotientGroup.mk' (toPrincipalIdeal R K').range) ((Units.mapEquiv ↑(FractionalIdeal.canonicalEquiv R⁰ K K')) I)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>K' : Type u_4<VAR>Field K'<VAR>Algebra R K'<VAR>IsFractionRing R K'<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>ClassGroup.mk ((Units.map ↑(FractionalIdeal.canonicalEquiv R⁰ K K')) I) = ClassGroup.mk I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>I : ↥(Ideal R)⁰<GOAL>↑((FractionalIdeal.mk0 K) I) = ↑↑I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>K' : Type u_4<VAR>Field K'<VAR>Algebra R K'<VAR>IsFractionRing R K'<VAR>I : ↥(Ideal R)⁰<GOAL>(FractionalIdeal.canonicalEquiv R⁰ K K') ↑((FractionalIdeal.mk0 K) I) = ↑((FractionalIdeal.mk0 K') I)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>K' : Type u_4<VAR>Field K'<VAR>Algebra R K'<VAR>IsFractionRing R K'<VAR>I : ↥(Ideal R)⁰<GOAL>(Units.map ↑(FractionalIdeal.canonicalEquiv R⁰ K K')) ((FractionalIdeal.mk0 K) I) = (FractionalIdeal.mk0 K') I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>I : ↥(Ideal R)⁰<GOAL>ClassGroup.mk ((FractionalIdeal.mk0 K) I) = ClassGroup.mk0 I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>I : ↥(Ideal R)⁰<GOAL>(ClassGroup.equiv K) (ClassGroup.mk0 I) = (QuotientGroup.mk' (toPrincipalIdeal R K).range) ((FractionalIdeal.mk0 K) I)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>ClassGroup.mk0 I = ClassGroup.mk0 J ↔ ∃ x, ∃ (_ : x ≠ 0), FractionalIdeal.spanSingleton R⁰ x * ↑↑I = ↑↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>ClassGroup.mk0 I = ClassGroup.mk0 J ↔ ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑J
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>I : FractionalIdeal R⁰ (FractionRing R)<VAR>hI : I ≠ 0<GOAL>I.num ∈ (Ideal R)⁰
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>I : (FractionalIdeal R⁰ (FractionRing R))ˣ<GOAL>ClassGroup.mk0 ⟨ClassGroup.integralRep ↑I, ⋯⟩ = ClassGroup.mk I
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsDedekindDomain R<GOAL>Function.Surjective ⇑ClassGroup.mk0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>CommRing R<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>ClassGroup.mk I = 1 ↔ (↑↑I).IsPrincipal
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>I : Ideal R<VAR>hI : I ∈ (Ideal R)⁰<GOAL>ClassGroup.mk0 ⟨I, hI⟩ = 1 ↔ Submodule.IsPrincipal I
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>I J : ↥(Ideal R)⁰<GOAL>ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<GOAL>Fintype.card (ClassGroup R) = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDomain R<VAR>IsDedekindDomain R<VAR>Fintype (ClassGroup R)<GOAL>Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R
<VAR>R : Type u_1<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>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<GOAL>IsIntegrallyClosedIn R B → IsIntegrallyClosedIn R A
<VAR>R : Type u_1<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>e : A ≃ₐ[R] B<GOAL>IsIntegrallyClosedIn R A ↔ IsIntegrallyClosedIn R B
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_4<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>IsIntegrallyClosed R ↔ IsIntegrallyClosedIn R K
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_4<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>IsIntegrallyClosed R ↔ IsIntegralClosure R R K
<VAR>R : Type u_5<VAR>A : Type u_6<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<GOAL>IsIntegrallyClosedIn R A ↔ Function.Injective ⇑(algebraMap R A) ∧ ∀ {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_4<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, (algebraMap R K) y = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>x : A<GOAL>IsIntegral R x → ∃ y, (algebraMap R A) y = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>x : A<GOAL>IsIntegral R x ↔ ∃ y, (algebraMap R A) y = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>x : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : IsIntegral R (x ^ n)<GOAL>∃ y, (algebraMap R A) y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_3<VAR>CommRing A<VAR>Algebra R A<VAR>S : Subalgebra R A<VAR>IsIntegrallyClosedIn (↥S) A<VAR>x : A<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : x ^ n ∈ S<GOAL>∃ y, (algebraMap (↥S) A) y = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>hRA : Function.Injective ⇑(algebraMap R A)<GOAL>integralClosure R A = ⊥ ↔ IsIntegrallyClosedIn R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>iic : IsIntegrallyClosedIn R A<VAR>NoZeroSMulDivisors R A<VAR>Nontrivial A<GOAL>integralClosure R A = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>IsIntegralClosure A R B<GOAL>IsIntegrallyClosedIn A B
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>B : Type u_3<VAR>CommRing B<VAR>Algebra R B<VAR>Algebra A B<VAR>IsScalarTower R A B<VAR>IsIntegrallyClosedIn A B<VAR>Algebra.IsIntegral R A<GOAL>IsIntegralClosure A R B
<VAR>R : Type u_1<VAR>CommRing R<VAR>iic : IsIntegrallyClosed R<VAR>K : Type u_3<VAR>CommRing K<VAR>Algebra R K<VAR>ifr : IsFractionRing R K<VAR>x : K<GOAL>IsIntegral R x → ∃ y, (algebraMap R K) y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>iic : IsIntegrallyClosed R<VAR>K : Type u_3<VAR>CommRing K<VAR>Algebra R K<VAR>ifr : IsFractionRing R K<VAR>x : K<GOAL>IsIntegral R x ↔ ∃ y, (algebraMap R K) y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>iic : IsIntegrallyClosed R<VAR>K : Type u_3<VAR>CommRing K<VAR>Algebra R K<VAR>ifr : IsFractionRing R K<VAR>x : K<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : IsIntegral R (x ^ n)<GOAL>∃ y, (algebraMap R K) y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_4<VAR>CommRing K<VAR>Algebra R K<VAR>S : Subalgebra R K<VAR>IsIntegrallyClosed ↥S<VAR>IsFractionRing (↥S) K<VAR>x : K<VAR>n : ℕ<VAR>hn : 0 < n<VAR>hx : x ^ n ∈ S<GOAL>∃ y, (algebraMap (↥S) K) y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_3<VAR>CommRing K<VAR>Algebra R K<VAR>ifr : IsFractionRing R K<GOAL>integralClosure R K = ⊥ ↔ IsIntegrallyClosed R
<VAR>R : Type u_1<VAR>CommRing R<VAR>id : IsDomain R<VAR>iic : IsIntegrallyClosed R<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a b : R<GOAL>a ^ n ∣ b ^ n ↔ a ∣ b
<VAR>R : Type u_1<VAR>CommRing R<VAR>iic : IsIntegrallyClosed R<VAR>K : Type u_3<VAR>CommRing K<VAR>Algebra R K<VAR>ifr : IsFractionRing R K<GOAL>integralClosure R K = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_2<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra K L<VAR>Algebra R L<VAR>IsScalarTower R K L<VAR>IsDomain R<VAR>FiniteDimensional K L<GOAL>IsIntegrallyClosed ↥(integralClosure R L)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal S<VAR>r : S<VAR>hr : r ∈ I<VAR>p : Polynomial R<VAR>hp : Polynomial.eval₂ f r p ∈ I<GOAL>p.coeff 0 ∈ Ideal.comap f I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal S<VAR>r : S<VAR>hr : r ∈ I<VAR>p : Polynomial R<VAR>hp : Polynomial.eval₂ f r p = 0<GOAL>p.coeff 0 ∈ Ideal.comap f I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal S<VAR>r : S<VAR>r_non_zero_divisor : ∀ {x : S}, x * r = 0 → x = 0<VAR>hr : r ∈ I<VAR>p : Polynomial R<GOAL>p ≠ 0 → Polynomial.eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ Ideal.comap f I
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Ideal (Polynomial R)<GOAL>Function.Injective ⇑(Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P) (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ⋯)
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Ideal (Polynomial R)<GOAL>((Ideal.Quotient.mk (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)).comp Polynomial.C).comp (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) = (Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P) (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ⋯).comp ((Ideal.Quotient.mk P).comp Polynomial.C)
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Ideal (Polynomial R)<VAR>Pb : P ≠ ⊥<VAR>hP : ∀ (x : R), Polynomial.C x ∈ P → x = 0<GOAL>∃ p ∈ P, Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) p ≠ 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>Algebra R S<VAR>Algebra (R ⧸ p) (S ⧸ P)<VAR>IsScalarTower R (R ⧸ p) (S ⧸ P)<VAR>h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))<GOAL>Ideal.comap (algebraMap R S) P = p
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>x : R<GOAL>(algebraMap (R ⧸ p) (S ⧸ Ideal.map f p)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk (Ideal.map f p)) (f x)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>x : R<VAR>y : S<GOAL>(Ideal.Quotient.mk p) x • (Ideal.Quotient.mk (Ideal.map f p)) y = (Ideal.Quotient.mk (Ideal.map f p)) (f x * y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I : Ideal S<VAR>IsDomain S<VAR>r : S<VAR>r_ne_zero : r ≠ 0<VAR>hr : r ∈ I<VAR>p : Polynomial R<GOAL>p ≠ 0 → Polynomial.eval₂ f r p = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ Ideal.comap f I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>hr : r ∈ ↑J \ ↑I<VAR>p : Polynomial R<VAR>p_ne_zero : Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0<VAR>hpI : Polynomial.eval₂ f r p ∈ I<GOAL>∃ i, p.coeff i ∈ ↑(Ideal.comap f J) \ ↑(Ideal.comap f I)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>I.IsPrime<VAR>hIJ : I ≤ J<VAR>r : S<VAR>hr : r ∈ ↑J \ ↑I<VAR>p : Polynomial R<VAR>p_ne_zero : Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p ≠ 0<VAR>hp : Polynomial.eval₂ f r p ∈ I<GOAL>Ideal.comap f I < Ideal.comap f J
<VAR>S : Type u_2<VAR>CommRing S<VAR>I : Ideal S<VAR>h : 1 ∈ I<VAR>x : S<GOAL>x ∈ I