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<VAR>P : Algebra.Generators R S<VAR>R₀ : Type u_1<VAR>CommRing R₀<VAR>Algebra R₀ S<VAR>r : R₀<VAR>x : P.Cotangent<GOAL>(r • x).val = P.σ ((algebraMap R₀ S) r) • x.val
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>r : S<VAR>x : P.Cotangent<GOAL>(r • x).val = P.σ r • x.val
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>r : P.Ring<VAR>x : P.Cotangent<GOAL>(r • x).val = r • x.val
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>r : R<VAR>x : P.Cotangent<GOAL>(r • x).val = r • x.val
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>x : ↥P.ker<GOAL>(Algebra.Generators.Cotangent.mk x).val = P.ker.toCotangent x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Function.Surjective ⇑Algebra.Generators.Cotangent.mk
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>f : P.Hom P'<VAR>x : ↥P.ker<GOAL>(Algebra.Generators.Cotangent.map f) (Algebra.Generators.Cotangent.mk x) = Algebra.Generators.Cotangent.mk ⟨f.toAlgHom ↑x, ⋯⟩
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<GOAL>Algebra.Generators.Cotangent.map (Algebra.Generators.Hom.id P) = LinearMap.id
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>P : Algebra.Generators R S<VAR>R' : Type u_1<VAR>S' : Type u_2<VAR>CommRing R'<VAR>CommRing S'<VAR>Algebra R' S'<VAR>P' : Algebra.Generators R' S'<VAR>Algebra R R'<VAR>Algebra S S'<VAR>Algebra R S'<VAR>IsScalarTower R R' S'<VAR>IsScalarTower R S S'<VAR>R'' : Type u_4<VAR>S'' : Type u_5<VAR>CommRing R''<VAR>CommRing S''<VAR>Algebra R'' S''<VAR>P'' : Algebra.Generators R'' S''<VAR>Algebra R R''<VAR>Algebra S S''<VAR>Algebra R S''<VAR>IsScalarTower R R'' S''<VAR>IsScalarTower R S S''<VAR>Algebra R' R''<VAR>Algebra S' S''<VAR>Algebra R' S''<VAR>IsScalarTower R' R'' S''<VAR>IsScalarTower R' S' S''<VAR>IsScalarTower R R' R''<VAR>IsScalarTower S S' S''<VAR>f : P.Hom P'<VAR>g : P'.Hom P''<GOAL>Algebra.Generators.Cotangent.map (g.comp f) = ↑S (Algebra.Generators.Cotangent.map g) ∘ₗ Algebra.Generators.Cotangent.map f
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>AddCommGroup V<VAR>Semiring R<VAR>Module R V<VAR>k : ℕ<VAR>f : LaurentSeries V<GOAL>(LaurentSeries.hasseDeriv R k) f = HahnSeries.ofSuppBddBelow (fun n => Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯
<VAR>R : Type u_1<VAR>Semiring R<VAR>V : Type u_2<VAR>AddCommGroup V<VAR>Module R V<VAR>k : ℕ<VAR>f : LaurentSeries V<VAR>n : ℤ<GOAL>((LaurentSeries.hasseDeriv R k) f).coeff n = Ring.choose (n + ↑k) k • f.coeff (n + ↑k)
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : PowerSeries R<VAR>n : ℕ<GOAL>((HahnSeries.ofPowerSeries ℤ R) x).coeff ↑n = (PowerSeries.coeff R n) x
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : LaurentSeries R<VAR>n : ℕ<GOAL>(PowerSeries.coeff R n) x.powerSeriesPart = x.coeff (HahnSeries.order x + ↑n)
<VAR>R : Type u_1<VAR>Semiring R<GOAL>LaurentSeries.powerSeriesPart 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : LaurentSeries R<GOAL>x.powerSeriesPart = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : LaurentSeries R<GOAL>(HahnSeries.single (HahnSeries.order x)) 1 * (HahnSeries.ofPowerSeries ℤ R) x.powerSeriesPart = x
<VAR>R : Type u_1<VAR>Semiring R<VAR>x : LaurentSeries R<GOAL>(HahnSeries.ofPowerSeries ℤ R) x.powerSeriesPart = (HahnSeries.single (-HahnSeries.order x)) 1 * x
<VAR>R : Type u_1<VAR>CommSemiring R<GOAL>⇑(algebraMap (PowerSeries R) (LaurentSeries R)) = ⇑(HahnSeries.ofPowerSeries ℤ R)
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(HahnSeries.ofPowerSeries ℤ R) 0 = 0
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(HahnSeries.ofPowerSeries ℤ R) 1 = 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : PowerSeries R<GOAL>(HahnSeries.ofPowerSeries ℤ R) (f + g) = (HahnSeries.ofPowerSeries ℤ R) f + (HahnSeries.ofPowerSeries ℤ R) g
<VAR>R' : Type u_2<VAR>Ring R'<VAR>f' g' : PowerSeries R'<GOAL>(HahnSeries.ofPowerSeries ℤ R') (f' - g') = (HahnSeries.ofPowerSeries ℤ R') f' - (HahnSeries.ofPowerSeries ℤ R') g'
<VAR>R' : Type u_2<VAR>Ring R'<VAR>f' : PowerSeries R'<GOAL>(HahnSeries.ofPowerSeries ℤ R') (-f') = -(HahnSeries.ofPowerSeries ℤ R') f'
<VAR>R : Type u_1<VAR>Semiring R<VAR>f g : PowerSeries R<GOAL>(HahnSeries.ofPowerSeries ℤ R) (f * g) = (HahnSeries.ofPowerSeries ℤ R) f * (HahnSeries.ofPowerSeries ℤ R) g
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : PowerSeries R<VAR>i : ℤ<GOAL>((HahnSeries.ofPowerSeries ℤ R) f).coeff i = if i < 0 then 0 else (PowerSeries.coeff R i.natAbs) f
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R<GOAL>(HahnSeries.ofPowerSeries ℤ R) ((PowerSeries.C R) r) = HahnSeries.C r
<VAR>R : Type u_1<VAR>Semiring R<GOAL>(HahnSeries.ofPowerSeries ℤ R) PowerSeries.X = (HahnSeries.single 1) 1
<VAR>R : Type u_1<VAR>Semiring R<VAR>S : Type u_3<VAR>Semiring S<VAR>Module R S<VAR>r : R<VAR>x : PowerSeries S<GOAL>(HahnSeries.ofPowerSeries ℤ S) (r • x) = r • (HahnSeries.ofPowerSeries ℤ S) x
<VAR>R : Type u_1<VAR>Semiring R<VAR>f : PowerSeries R<VAR>n : ℕ<GOAL>(HahnSeries.ofPowerSeries ℤ R) (f ^ n) = (HahnSeries.ofPowerSeries ℤ R) f ^ n
<VAR>F : Type u<VAR>Field F<VAR>f : RatFunc F<GOAL>↑f = (RatFunc.coeAlgHom F) f
<VAR>F : Type u<VAR>Field F<VAR>f : RatFunc F<GOAL>↑f = (HahnSeries.ofPowerSeries ℤ F) ↑f.num / (HahnSeries.ofPowerSeries ℤ F) ↑f.denom
<VAR>F : Type u<VAR>Field F<GOAL>Function.Injective RatFunc.coeToLaurentSeries_fun
<VAR>F : Type u<VAR>Field F<VAR>f : RatFunc F<GOAL>(RatFunc.coeAlgHom F) f = ↑f
<VAR>F : Type u<VAR>Field F<VAR>P : F[X]<GOAL>(HahnSeries.ofPowerSeries ℤ F) ↑P = ↑↑P
<VAR>F : Type u<VAR>Field F<GOAL>↑0 = 0
<VAR>F : Type u<VAR>Field F<VAR>f : F[X]<VAR>hf : f ≠ 0<GOAL>↑f ≠ 0
<VAR>F : Type u<VAR>Field F<GOAL>↑1 = 1
<VAR>F : Type u<VAR>Field F<VAR>f g : RatFunc F<GOAL>↑(f + g) = ↑f + ↑g
<VAR>F : Type u<VAR>Field F<VAR>f g : RatFunc F<GOAL>↑(f - g) = ↑f - ↑g
<VAR>F : Type u<VAR>Field F<VAR>f : RatFunc F<GOAL>↑(-f) = -↑f
<VAR>F : Type u<VAR>Field F<VAR>f g : RatFunc F<GOAL>↑(f * g) = ↑f * ↑g
<VAR>F : Type u<VAR>Field F<VAR>f : RatFunc F<VAR>n : ℕ<GOAL>↑(f ^ n) = ↑f ^ n
<VAR>F : Type u<VAR>Field F<VAR>f g : RatFunc F<GOAL>↑(f / g) = ↑f / ↑g
<VAR>F : Type u<VAR>Field F<VAR>r : F<GOAL>↑(RatFunc.C r) = HahnSeries.C r
<VAR>F : Type u<VAR>Field F<VAR>f : RatFunc F<VAR>r : F<GOAL>↑(r • f) = r • ↑f
<VAR>F : Type u<VAR>Field F<GOAL>↑RatFunc.X = (HahnSeries.single 1) 1
<VAR>R : Type u_2<VAR>Ring R<VAR>n : ℕ<GOAL>(HahnSeries.single ↑n) 1 = (HahnSeries.single 1) 1 ^ n
<VAR>F : Type u<VAR>Field F<VAR>d : ℤ<VAR>α : F<VAR>hα : α ≠ 0<GOAL>(HahnSeries.single (-d)) α⁻¹ = ((HahnSeries.single d) α)⁻¹
<VAR>F : Type u<VAR>Field F<VAR>n : ℤ<GOAL>(HahnSeries.single n) 1 = (HahnSeries.single 1) 1 ^ n
<VAR>F : Type u<VAR>Field F<VAR>p q : F[X]<GOAL>(algebraMap (RatFunc F) (LaurentSeries F)) ((algebraMap F[X] (RatFunc F)) p / (algebraMap F[X] (RatFunc F)) q) = (algebraMap F[X] (LaurentSeries F)) p / (algebraMap F[X] (LaurentSeries F)) q
<VAR>K : Type u_2<VAR>Field K<VAR>P : K[X]<GOAL>(Polynomial.idealX K).intValuation P = (PowerSeries.idealX K).intValuation ↑P
<VAR>K : Type u_2<VAR>Field K<GOAL>(PowerSeries.idealX K).intValuationDef PowerSeries.X = ↑(Multiplicative.ofAdd (-1))
<VAR>K : Type u_2<VAR>Field K<VAR>P : RatFunc K<GOAL>(Polynomial.idealX K).valuation P = (PowerSeries.idealX K).valuation ↑P
<VAR>K : Type u_2<VAR>Field K<VAR>s : ℕ<GOAL>Valued.v ((HahnSeries.ofPowerSeries ℤ K) PowerSeries.X ^ s) = ↑(Multiplicative.ofAdd (-↑s))
<VAR>K : Type u_2<VAR>Field K<VAR>s : ℤ<GOAL>Valued.v ((HahnSeries.single s) 1) = ↑(Multiplicative.ofAdd (-s))
<VAR>K : Type u_2<VAR>Field K<VAR>n d : ℕ<VAR>f : PowerSeries K<VAR>H : Valued.v ((HahnSeries.ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))<GOAL>n < d → (PowerSeries.coeff K n) f = 0
<VAR>K : Type u_2<VAR>Field K<VAR>d : ℕ<VAR>f : PowerSeries K<GOAL>Valued.v ((HahnSeries.ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d)) ↔ ∀ n < d, (PowerSeries.coeff K n) f = 0
<VAR>K : Type u_2<VAR>Field K<VAR>n D : ℤ<VAR>f : LaurentSeries K<VAR>H : Valued.v f ≤ ↑(Multiplicative.ofAdd (-D))<GOAL>n < D → f.coeff n = 0
<VAR>K : Type u_2<VAR>Field K<VAR>D : ℤ<VAR>f : LaurentSeries K<GOAL>Valued.v f ≤ ↑(Multiplicative.ofAdd (-D)) ↔ ∀ n < D, f.coeff n = 0
<VAR>K : Type u_2<VAR>Field K<VAR>d n : ℤ<VAR>f g : LaurentSeries K<VAR>H : Valued.v (g - f) ≤ ↑(Multiplicative.ofAdd (-d))<GOAL>n < d → g.coeff n = f.coeff n
<VAR>K : Type u_2<VAR>Field K<VAR>f : LaurentSeries K<GOAL>Valued.v f ≤ 1 ↔ ∃ F, (HahnSeries.ofPowerSeries ℤ K) F = f
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>self : Module.Free R M<GOAL>Nonempty ((I : Type v) × Basis I R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Small.{w, v} M<GOAL>Module.Free R M ↔ ∃ I, Nonempty (Basis I R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Module.Free R M ↔ ∃ S, Nonempty (Basis (↑S) R M)
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type w<VAR>b : Basis ι R M<GOAL>Module.Free R M
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Free R M<VAR>Infinite R<VAR>Nontrivial M<GOAL>Infinite M
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type z<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module.Free R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>e : M ≃ₗ[R] N<GOAL>Module.Free R N
<VAR>R : Type u<VAR>N : Type z<VAR>Semiring R<VAR>AddCommMonoid N<VAR>Module R N<VAR>P : Type v<VAR>AddCommMonoid P<VAR>Module R P<GOAL>Module.Free R P → (P ≃ₗ[R] N) → Module.Free R N
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Ring R<VAR>Ring S<VAR>e : R ≃+* S<VAR>IsSemisimpleRing R<GOAL>IsSemisimpleRing S
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSimpleModule R M<GOAL>Nontrivial M
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Ring R<VAR>Ring S<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module S N<VAR>σ : R →+* S<VAR>RingHomSurjective σ<VAR>l : M →ₛₗ[σ] N<VAR>hl : Function.Bijective ⇑l<GOAL>IsSimpleModule R M ↔ IsSimpleModule S N
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>l : M ≃ₗ[R] N<VAR>IsSimpleModule R N<GOAL>IsSimpleModule R M
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>m : Submodule R M<GOAL>IsSimpleModule R ↥m ↔ IsAtom m
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>m : Submodule R M<GOAL>IsSimpleModule R (M ⧸ m) ↔ IsCoatom m
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>A B : Submodule R M<VAR>hAB : A ≤ B<GOAL>A ⋖ B ↔ IsSimpleModule R (↥B ⧸ Submodule.comap B.subtype A)
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>m : Submodule R M<VAR>IsSimpleModule R ↥m<GOAL>IsAtom m
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSimpleModule R M<VAR>m : M<VAR>hm : m ≠ 0<GOAL>Submodule.span R {m} = ⊤
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSimpleModule R M<VAR>m : M<VAR>hm : m ≠ 0<GOAL>Function.Surjective ⇑(LinearMap.toSpanSingleton R M m)
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSimpleModule R M<VAR>m : M<VAR>hm : m ≠ 0<GOAL>Ideal.IsMaximal (LinearMap.ker (LinearMap.toSpanSingleton R M m))
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsSimpleModule R M ↔ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>R : Type u_6<VAR>CommRing R<VAR>Module R M<VAR>simple : IsSimpleModule R M<GOAL>(Module.annihilator R M).IsMaximal
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<GOAL>IsSimpleModule R M ↔ Nontrivial M ∧ ∀ (x : M), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R M x)
<VAR>R : Type u_2<VAR>Ring R<GOAL>IsSimpleModule R R ↔ Nontrivial R ∧ ∀ (x : R), x ≠ 0 → IsUnit x
<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>R : Type u_6<VAR>DivisionRing R<VAR>Module R M<GOAL>IsSimpleModule R M ↔ FiniteDimensional.finrank R M = 1
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>h : sSup {m | IsSimpleModule R ↥m} = ⊤<GOAL>IsSemisimpleModule R M
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSemisimpleModule R M<VAR>N : Submodule R M<GOAL>N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R ↥m
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSemisimpleModule R M<VAR>N : Submodule R M<GOAL>sSup {m | IsSimpleModule R ↥m ∧ m ≤ N} = N
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSemisimpleModule R M<VAR>Nontrivial M<GOAL>∃ m, IsSimpleModule R ↥m
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>IsSemisimpleModule R M<GOAL>sSup {m | IsSimpleModule R ↥m} = ⊤
<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>R : Type u_6<VAR>CommRing R<VAR>Module R M<VAR>IsSemisimpleModule R M<GOAL>(Module.annihilator R M).IsRadical
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSemisimpleModule R N<VAR>e : M ≃ₗ[R] N<GOAL>IsSemisimpleModule R M
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSemisimpleModule R M<VAR>f : M →ₗ[R] N<GOAL>IsSemisimpleModule R ↥(LinearMap.range f)
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Ring R<VAR>Ring S<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module S N<VAR>σ : R →+* S<VAR>RingHomSurjective σ<VAR>l : M →ₛₗ[σ] N<VAR>hl : Function.Bijective ⇑l<GOAL>IsSemisimpleModule R M ↔ IsSemisimpleModule S N
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<GOAL>sSup {m | IsSimpleModule R ↥m} = ⊤ ↔ IsSemisimpleModule R M
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)<VAR>hp' : ⨆ i ∈ s, p i = ⊤<GOAL>IsSemisimpleModule R M
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>s : Set ι<VAR>p : ι → Submodule R M<VAR>hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)<GOAL>IsSemisimpleModule R ↥(⨆ i ∈ s, p i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>p : ι → Submodule R M<VAR>hp : ∀ (i : ι), IsSemisimpleModule R ↥(p i)<VAR>hp' : ⨆ i, p i = ⊤<GOAL>IsSemisimpleModule R M
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>IsSemisimpleModule R ↥p → IsSemisimpleModule R ↥q → IsSemisimpleModule R ↥(p ⊔ q)
<VAR>R : Type u_2<VAR>S : Type u_3<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>IsSemisimpleRing R<GOAL>IsSemisimpleRing S
<VAR>R : Type u_2<VAR>Ring R<VAR>IsSemisimpleRing R<VAR>I : Ideal R<GOAL>∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSimpleModule R M<VAR>f : M →ₗ[R] N<GOAL>Function.Injective ⇑f ∨ f = 0
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSimpleModule R M<VAR>f : M →ₗ[R] N<VAR>h : f ≠ 0<GOAL>Function.Injective ⇑f
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSimpleModule R N<VAR>f : M →ₗ[R] N<GOAL>Function.Surjective ⇑f ∨ f = 0
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSimpleModule R N<VAR>f : M →ₗ[R] N<VAR>h : f ≠ 0<GOAL>Function.Surjective ⇑f
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSimpleModule R M<VAR>IsSimpleModule R N<VAR>f : M →ₗ[R] N<GOAL>Function.Bijective ⇑f ∨ f = 0
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSimpleModule R M<VAR>IsSimpleModule R N<VAR>f : M →ₗ[R] N<VAR>h : f ≠ 0<GOAL>Function.Bijective ⇑f
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>IsSimpleModule R N<VAR>f : M →ₗ[R] N<VAR>hf : Function.Surjective ⇑f<GOAL>IsCoatom (LinearMap.ker f)
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>X Y : Submodule R M × Submodule R M<GOAL>JordanHolderModule.Iso X Y → JordanHolderModule.Iso Y X
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>X Y Z : Submodule R M × Submodule R M<GOAL>JordanHolderModule.Iso X Y → JordanHolderModule.Iso Y Z → JordanHolderModule.Iso X Z
<VAR>R : Type u_2<VAR>Ring R<VAR>M : Type u_4<VAR>AddCommGroup M<VAR>Module R M<VAR>X Y : Submodule R M<GOAL>X ⋖ X ⊔ Y → JordanHolderModule.Iso (X, X ⊔ Y) (X ⊓ Y, Y)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>f : R →+* S<VAR>r : R<GOAL>f.kerLift ((Ideal.Quotient.mk (RingHom.ker f)) r) = f r
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<VAR>hI : RingHom.ker f ≤ I<GOAL>Function.Injective ⇑(Ideal.Quotient.lift I f H)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>f : R →+* S<GOAL>Function.Injective ⇑f.kerLift
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>f : R →+* S<VAR>g : S → R<VAR>hf : Function.RightInverse g ⇑f<VAR>x : R ⧸ RingHom.ker f<GOAL>(RingHom.quotientKerEquivOfRightInverse hf) x = f.kerLift x
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>f : R →+* S<VAR>g : S → R<VAR>hf : Function.RightInverse g ⇑f<VAR>x : S<GOAL>(RingHom.quotientKerEquivOfRightInverse hf).symm x = (Ideal.Quotient.mk (RingHom.ker f)) (g x)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>Ideal.map (Ideal.Quotient.mk I) I = ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>RingHom.ker (Ideal.Quotient.mk I) = I
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : I ≤ J<GOAL>Ideal.map (Ideal.Quotient.mk J) I = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : I ≤ RingHom.ker f<GOAL>RingHom.ker (Ideal.Quotient.lift I f H) = Ideal.map (Ideal.Quotient.mk I) (RingHom.ker f)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Semiring S<VAR>I : Ideal R<VAR>f : R →+* S<VAR>H : ∀ a ∈ I, f a = 0<GOAL>Function.Injective ⇑(Ideal.Quotient.lift I f H) ↔ RingHom.ker f = I
<VAR>R : Type u<VAR>CommRing R<VAR>ι : Type u_1<VAR>I : ι → Ideal R<GOAL>RingHom.ker (Pi.ringHom fun i => Ideal.Quotient.mk (I i)) = ⨅ i, I i
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>⊥.IsMaximal ↔ I.IsMaximal
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>x : R<GOAL>(Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J ⊔ I
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>hIJ : I ≤ J<VAR>x : R<GOAL>(Ideal.Quotient.mk I) x ∈ Ideal.map (Ideal.Quotient.mk I) J ↔ x ∈ J
<VAR>R : Type u<VAR>CommRing R<VAR>ι : Type u_1<VAR>I : ι → Ideal R<VAR>x : R<GOAL>(Ideal.quotientInfToPiQuotient I) ((Ideal.Quotient.mk (⨅ i, I i)) x) = fun i => (Ideal.Quotient.mk (I i)) x
<VAR>R : Type u<VAR>CommRing R<VAR>ι : Type u_1<VAR>I : ι → Ideal R<VAR>x : R<VAR>i : ι<GOAL>(Ideal.quotientInfToPiQuotient I) ((Ideal.Quotient.mk (⨅ i, I i)) x) i = (Ideal.Quotient.mk (I i)) x
<VAR>R : Type u<VAR>CommRing R<VAR>ι : Type u_1<VAR>I : ι → Ideal R<GOAL>Function.Injective ⇑(Ideal.quotientInfToPiQuotient I)
<VAR>R : Type u<VAR>CommRing R<VAR>ι : Type u_1<VAR>Finite ι<VAR>I : ι → Ideal R<VAR>hI : Pairwise fun i j => IsCoprime (I i) (I j)<GOAL>Function.Surjective ⇑(Ideal.quotientInfToPiQuotient I)
<VAR>R : Type u_2<VAR>CommRing R<VAR>ι : Type u_3<VAR>Finite ι<VAR>I : ι → Ideal R<VAR>hf : Pairwise fun i j => IsCoprime (I i) (I j)<VAR>x : (i : ι) → R ⧸ I i<GOAL>∃ r, ∀ (i : ι), (Ideal.Quotient.mk (I i)) r = x i
<VAR>R : Type u_2<VAR>CommRing R<VAR>ι : Type u_3<VAR>Finite ι<VAR>I : ι → Ideal R<VAR>hI : Pairwise fun i j => IsCoprime (I i) (I j)<VAR>x : ι → R<GOAL>∃ r, ∀ (i : ι), r - x i ∈ I i
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<VAR>x : R ⧸ I ⊓ J<GOAL>((I.quotientInfEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor (I ⊓ J) I ⋯) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<VAR>x : R ⧸ I ⊓ J<GOAL>((I.quotientInfEquivQuotientProd J coprime) x).2 = (Ideal.Quotient.factor (I ⊓ J) J ⋯) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>(RingHom.fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = Ideal.Quotient.factor (I ⊓ J) I ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>(RingHom.snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = Ideal.Quotient.factor (I ⊓ J) J ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<VAR>x : R ⧸ I * J<GOAL>((I.quotientMulEquivQuotientProd J coprime) x).1 = (Ideal.Quotient.factor (I * J) I ⋯) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<VAR>x : R ⧸ I * J<GOAL>((I.quotientMulEquivQuotientProd J coprime) x).2 = (Ideal.Quotient.factor (I * J) J ⋯) x
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>(RingHom.fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = Ideal.Quotient.factor (I * J) I ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>coprime : IsCoprime I J<GOAL>(RingHom.snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = Ideal.Quotient.factor (I * J) J ⋯
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I : Ideal A<VAR>S : Type u_5<VAR>Semiring S<VAR>Algebra R₁ S<VAR>f g : A ⧸ I →ₐ[R₁] S<VAR>h : f.comp (Ideal.Quotient.mkₐ R₁ I) = g.comp (Ideal.Quotient.mkₐ R₁ I)<GOAL>f = g
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I : Ideal A<GOAL>algebraMap R₁ (A ⧸ I) = (algebraMap A (A ⧸ I)).comp (algebraMap R₁ A)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I : Ideal A<GOAL>(Ideal.Quotient.mkₐ R₁ I).toRingHom = Ideal.Quotient.mk I
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I : Ideal A<GOAL>⇑(Ideal.Quotient.mkₐ R₁ I) = ⇑(Ideal.Quotient.mk I)
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<GOAL>algebraMap R (R ⧸ I) = Ideal.Quotient.mk I
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I : Ideal A<GOAL>(Ideal.Quotient.mk I).comp (algebraMap R₁ A) = algebraMap R₁ (A ⧸ I)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I : Ideal A<VAR>x : R₁<GOAL>(Ideal.Quotient.mk I) ((algebraMap R₁ A) x) = (algebraMap R₁ (A ⧸ I)) x
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I : Ideal A<GOAL>Function.Surjective ⇑(Ideal.Quotient.mkₐ R₁ I)
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>I : Ideal A<GOAL>RingHom.ker ↑(Ideal.Quotient.mkₐ R₁ I) = I
<VAR>R₁ : Type u_1<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R₁<VAR>CommRing A<VAR>Algebra R₁ A<VAR>Semiring B<VAR>Algebra R₁ B<VAR>I : Ideal A<VAR>f : A →ₐ[R₁] B<VAR>hI : ∀ a ∈ I, f a = 0<VAR>x : A ⧸ I<GOAL>(Ideal.Quotient.liftₐ I f hI) x = (Ideal.Quotient.lift I (↑f) hI) x