ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>Zero Γ<VAR>PartialOrder Γ<VAR>Zero R<VAR>One R<GOAL>(HahnSeries.single 0) 1 = 1
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>Zero Γ<VAR>PartialOrder Γ<VAR>MulZeroOneClass R<VAR>Nontrivial R<GOAL>HahnSeries.support 1 = {0}
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>Zero Γ<VAR>PartialOrder Γ<VAR>MulZeroOneClass R<VAR>Nontrivial R<GOAL>HahnSeries.orderTop 1 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>Zero Γ<VAR>PartialOrder Γ<VAR>MulZeroOneClass R<GOAL>HahnSeries.order 1 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>Zero Γ<VAR>PartialOrder Γ<VAR>MulZeroOneClass R<GOAL>HahnSeries.leadingCoeff 1 = 1
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>Zero V<VAR>SMul R V<VAR>x y : HahnModule Γ R V<VAR>h : ((HahnModule.of R).symm x).coeff = ((HahnModule.of R).symm y).coeff<GOAL>x = y
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>Zero V<VAR>SMul R V<VAR>x y : HahnModule Γ R V<GOAL>((HahnModule.of R).symm x).coeff = ((HahnModule.of R).symm y).coeff ↔ x = y
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>AddCommMonoid V<VAR>SMul R V<GOAL>(HahnModule.of R) 0 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>AddCommMonoid V<VAR>SMul R V<VAR>x y : HahnSeries Γ V<GOAL>(HahnModule.of R) (x + y) = (HahnModule.of R) x + (HahnModule.of R) y
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>AddCommMonoid V<VAR>SMul R V<GOAL>(HahnModule.of R).symm 0 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>AddCommMonoid V<VAR>SMul R V<VAR>x y : HahnModule Γ R V<GOAL>(HahnModule.of R).symm (x + y) = (HahnModule.of R).symm x + (HahnModule.of R).symm y
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>AddCommMonoid V<VAR>SMul R V<VAR>PartialOrder Γ'<VAR>VAdd Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>Zero R<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<GOAL>((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal ⋯ ⋯ a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>AddCommMonoid V<VAR>SMulZeroClass R V<VAR>r : R<VAR>x : HahnSeries Γ V<GOAL>(HahnModule.of R) (r • x) = r • (HahnModule.of R) x
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>V : Type u_4<VAR>AddCommMonoid V<VAR>PartialOrder Γ<VAR>SMulZeroClass R V<VAR>r : R<VAR>x : HahnModule Γ R V<GOAL>(HahnModule.of R).symm (r • x) = r • (HahnModule.of R).symm x
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>PartialOrder Γ'<VAR>VAdd Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>Zero R<VAR>AddCommMonoid V<VAR>SMulZeroClass R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ'<VAR>hs : s.IsPWO<VAR>hys : ((HahnModule.of R).symm y).support ⊆ s<GOAL>((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal ⋯ hs a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>PartialOrder Γ'<VAR>VAdd Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>Zero R<VAR>AddCommMonoid V<VAR>SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<VAR>a : Γ'<VAR>s : Set Γ<VAR>hs : s.IsPWO<VAR>hxs : x.support ⊆ s<GOAL>((HahnModule.of R).symm (x • y)).coeff a = ∑ ij ∈ Finset.VAddAntidiagonal hs ⋯ a, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>PartialOrder Γ'<VAR>VAdd Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>AddCommMonoid V<VAR>Zero R<VAR>DistribSMul R V<VAR>x : HahnSeries Γ R<VAR>y z : HahnModule Γ' R V<GOAL>x • (y + z) = x • y + x • z
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>PartialOrder Γ'<VAR>VAdd Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>AddCommMonoid V<VAR>AddCommMonoid R<VAR>SMulWithZero R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<VAR>h : ∀ (r s : R) (u : V), (r + s) • u = r • u + s • u<GOAL>(x + y) • z = x • z + y • z
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>PartialOrder Γ'<VAR>VAdd Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>AddCommMonoid V<VAR>MulZeroClass R<VAR>SMulWithZero R V<VAR>r : R<VAR>x : HahnModule Γ' R V<VAR>a : Γ'<VAR>b : Γ<GOAL>((HahnModule.of R).symm ((HahnSeries.single b) r • x)).coeff (b +ᵥ a) = r • ((HahnModule.of R).symm x).coeff a
<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ'<VAR>AddCommMonoid V<VAR>Γ : Type u_5<VAR>OrderedAddCommMonoid Γ<VAR>AddAction Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>MulZeroClass R<VAR>SMulWithZero R V<VAR>r : R<VAR>x : HahnModule Γ' R V<VAR>a : Γ'<GOAL>((HahnModule.of R).symm ((HahnSeries.single 0) r • x)).coeff a = r • ((HahnModule.of R).symm x).coeff a
<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ'<VAR>AddCommMonoid V<VAR>Γ : Type u_5<VAR>OrderedAddCommMonoid Γ<VAR>AddAction Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>MulZeroClass R<VAR>SMulWithZero R V<VAR>r : R<VAR>x : HahnModule Γ' R V<GOAL>(HahnSeries.single 0) r • x = r • x
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>PartialOrder Γ'<VAR>VAdd Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>AddCommMonoid V<VAR>Zero R<VAR>SMulWithZero R V<VAR>x : HahnModule Γ' R V<GOAL>0 • x = 0
<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ'<VAR>AddCommMonoid V<VAR>Γ : Type u_5<VAR>OrderedAddCommMonoid Γ<VAR>AddAction Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>MonoidWithZero R<VAR>MulActionWithZero R V<VAR>x : HahnModule Γ' R V<GOAL>1 • x = x
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>PartialOrder Γ<VAR>PartialOrder Γ'<VAR>VAdd Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>AddCommMonoid V<VAR>MulZeroClass R<VAR>SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ' R V<GOAL>((HahnModule.of R).symm (x • y)).support ⊆ x.support +ᵥ ((HahnModule.of R).symm y).support
<VAR>R : Type u_3<VAR>V : Type u_4<VAR>AddCommMonoid V<VAR>Γ : Type u_5<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>Zero R<VAR>SMulWithZero R V<VAR>x : HahnSeries Γ R<VAR>y : HahnModule Γ R V<GOAL>((HahnModule.of R).symm (x • y)).coeff (x.order + ((HahnModule.of R).symm y).order) = x.leadingCoeff • ((HahnModule.of R).symm y).leadingCoeff
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<GOAL>(HahnModule.of R).symm (x • (HahnModule.of R) y) = x * y
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<GOAL>(x * y).coeff a = ∑ ij ∈ Finset.addAntidiagonal ⋯ ⋯ a, x.coeff ij.1 * y.coeff ij.2
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<VAR>s : Set Γ<VAR>hs : s.IsPWO<VAR>hxs : x.support ⊆ s<GOAL>(x * y).coeff a = ∑ ij ∈ Finset.addAntidiagonal hs ⋯ a, x.coeff ij.1 * y.coeff ij.2
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<VAR>a : Γ<VAR>s : Set Γ<VAR>hs : s.IsPWO<VAR>hys : y.support ⊆ s<GOAL>(x * y).coeff a = ∑ ij ∈ Finset.addAntidiagonal ⋯ hs a, x.coeff ij.1 * y.coeff ij.2
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a b : Γ<GOAL>((HahnSeries.single b) r * x).coeff (a + b) = r * x.coeff a
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a b : Γ<GOAL>(x * (HahnSeries.single b) r).coeff (a + b) = x.coeff a * r
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a : Γ<GOAL>(x * (HahnSeries.single 0) r).coeff a = x.coeff a * r
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>r : R<VAR>x : HahnSeries Γ R<VAR>a : Γ<GOAL>((HahnSeries.single 0) r * x).coeff a = r * x.coeff a
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>Semiring R<VAR>r : R<VAR>x : HahnSeries Γ R<GOAL>(HahnSeries.single 0) r * x = r • x
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<GOAL>(x * y).support ⊆ x.support + y.support
<VAR>R : Type u_3<VAR>Γ : Type u_5<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<GOAL>(x * y).coeff (x.order + y.order) = x.leadingCoeff * y.leadingCoeff
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalSemiring R<VAR>x y z : HahnSeries Γ R<GOAL>x * y * z = x * (y * z)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>OrderedCancelAddCommMonoid Γ<VAR>PartialOrder Γ'<VAR>AddAction Γ Γ'<VAR>IsOrderedCancelVAdd Γ Γ'<VAR>AddCommMonoid V<VAR>Semiring R<VAR>Module R V<VAR>x y : HahnSeries Γ R<VAR>z : HahnModule Γ' R V<GOAL>(x * y) • z = x • y • z
<VAR>R : Type u_3<VAR>Γ : Type u_5<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>x y : HahnSeries Γ R<GOAL>x.orderTop + y.orderTop ≤ (x * y).orderTop
<VAR>R : Type u_3<VAR>Γ : Type u_5<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>NoZeroDivisors R<VAR>x y : HahnSeries Γ R<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(x * y).order = x.order + y.order
<VAR>R : Type u_3<VAR>Γ : Type u_5<VAR>LinearOrderedCancelAddCommMonoid Γ<VAR>Semiring R<VAR>NoZeroDivisors R<VAR>x : HahnSeries Γ R<VAR>n : ℕ<GOAL>(x ^ n).order = n • x.order
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonUnitalNonAssocSemiring R<VAR>a b : Γ<VAR>r s : R<GOAL>(HahnSeries.single a) r * (HahnSeries.single b) s = (HahnSeries.single (a + b)) (r * s)
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>Semiring R<VAR>a : Γ<VAR>n : ℕ<VAR>r : R<GOAL>(HahnSeries.single a) r ^ n = (HahnSeries.single (n • a)) (r ^ n)
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonAssocSemiring R<VAR>a : R<GOAL>HahnSeries.C a = (HahnSeries.single 0) a
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonAssocSemiring R<GOAL>HahnSeries.C 0 = 0
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonAssocSemiring R<GOAL>HahnSeries.C 1 = 1
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonAssocSemiring R<GOAL>Function.Injective ⇑HahnSeries.C
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonAssocSemiring R<VAR>r : R<VAR>h : r ≠ 0<GOAL>HahnSeries.C r ≠ 0
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>NonAssocSemiring R<VAR>r : R<GOAL>(HahnSeries.C r).order = 0
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>Semiring R<VAR>r : R<VAR>x : HahnSeries Γ R<GOAL>HahnSeries.C r * x = r • x
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>Γ' : Type u_5<VAR>OrderedCancelAddCommMonoid Γ'<VAR>NonUnitalNonAssocSemiring R<VAR>f : Γ ↪o Γ'<VAR>hf : ∀ (x y : Γ), f (x + y) = f x + f y<VAR>x y : HahnSeries Γ R<GOAL>HahnSeries.embDomain f (x * y) = HahnSeries.embDomain f x * HahnSeries.embDomain f y
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>Γ' : Type u_5<VAR>OrderedCancelAddCommMonoid Γ'<VAR>NonAssocSemiring R<VAR>f : Γ ↪o Γ'<VAR>hf : f 0 = 0<GOAL>HahnSeries.embDomain f 1 = 1
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>Γ' : Type u_5<VAR>OrderedCancelAddCommMonoid Γ'<VAR>NonAssocSemiring R<VAR>f : Γ →+ Γ'<VAR>hfi : Function.Injective ⇑f<VAR>hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'<GOAL>∀ (a : HahnSeries Γ R), (HahnSeries.embDomainRingHom f hfi hf) a = HahnSeries.embDomain { toFun := ⇑f, inj' := hfi, map_rel_iff' := ⋯ } a
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>Γ' : Type u_5<VAR>OrderedCancelAddCommMonoid Γ'<VAR>NonAssocSemiring R<VAR>f : Γ →+ Γ'<VAR>hfi : Function.Injective ⇑f<VAR>hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'<VAR>r : R<GOAL>(HahnSeries.embDomainRingHom f hfi hf) (HahnSeries.C r) = HahnSeries.C r
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>CommSemiring R<GOAL>HahnSeries.C = algebraMap R (HahnSeries Γ R)
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>CommSemiring R<VAR>A : Type u_5<VAR>Semiring A<VAR>Algebra R A<VAR>r : R<GOAL>(algebraMap R (HahnSeries Γ A)) r = HahnSeries.C ((algebraMap R A) r)
<VAR>Γ : Type u_1<VAR>R : Type u_3<VAR>OrderedCancelAddCommMonoid Γ<VAR>CommSemiring R<VAR>A : Type u_5<VAR>Semiring A<VAR>Algebra R A<VAR>Γ' : Type u_6<VAR>OrderedCancelAddCommMonoid Γ'<VAR>f : Γ →+ Γ'<VAR>hfi : Function.Injective ⇑f<VAR>hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'<GOAL>∀ (a : HahnSeries Γ A) (b : Γ'), ((HahnSeries.embDomainAlgHom f hfi hf) a).coeff b = if h : ∃ x, ¬a.coeff x = 0 ∧ f x = b then a.coeff (Classical.choose ⋯) else 0
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<VAR>self : Algebra.IsIntegral R A<VAR>x : A<GOAL>IsIntegral R x
<VAR>R : Type u_1<VAR>A : Type u_3<VAR>CommRing R<VAR>Ring A<VAR>Algebra R A<GOAL>Algebra.IsIntegral R A ↔ ∀ (x : A), IsIntegral R x
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal S<GOAL>↑(Ideal.comap f I) = ⇑f ⁻¹' ↑I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>f : F<VAR>I J : Ideal R<VAR>h : I ≤ J<GOAL>Ideal.map f I ≤ Ideal.map f J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>f : F<VAR>I : Ideal R<VAR>x : R<VAR>h : x ∈ I<GOAL>f x ∈ Ideal.map f I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>f : F<VAR>I : Ideal R<VAR>x : ↥I<GOAL>f ↑x ∈ Ideal.map f I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>K : Ideal S<GOAL>Ideal.map f I ≤ K ↔ I ≤ Ideal.comap f K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K : Ideal S<VAR>x : R<GOAL>x ∈ Ideal.comap f K ↔ f x ∈ K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K L : Ideal S<VAR>h : K ≤ L<GOAL>Ideal.comap f K ≤ Ideal.comap f L
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K : Ideal S<VAR>hK : K ≠ ⊤<GOAL>Ideal.comap f K ≠ ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>f : F<VAR>G : Type u_2<VAR>FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>g : G<VAR>I : Ideal R<VAR>hf : Set.LeftInvOn ⇑g ⇑f ↑I<GOAL>Ideal.map f I ≤ Ideal.comap g I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>G : Type u_2<VAR>FunLike G S R<VAR>g : G<VAR>I : Ideal S<VAR>hf : Set.LeftInvOn (⇑g) (⇑f) (⇑f ⁻¹' ↑I)<GOAL>Ideal.comap f I ≤ Ideal.map g I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>f : F<VAR>G : Type u_2<VAR>FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>g : G<VAR>I : Ideal R<VAR>h : Function.LeftInverse ⇑g ⇑f<GOAL>Ideal.map f I ≤ Ideal.comap g I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>G : Type u_2<VAR>FunLike G S R<VAR>g : G<VAR>I : Ideal S<VAR>h : Function.LeftInverse ⇑g ⇑f<GOAL>Ideal.comap f I ≤ Ideal.map g I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<GOAL>Ideal.map f ⊤ = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<GOAL>GaloisConnection (Ideal.map f) (Ideal.comap f)
<VAR>R : Type u<VAR>Semiring R<VAR>I : Ideal R<GOAL>Ideal.comap (RingHom.id R) I = I
<VAR>R : Type u<VAR>Semiring R<VAR>I : Ideal R<GOAL>Ideal.map (RingHom.id R) I = I
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>T : Type u_3<VAR>Semiring T<VAR>I : Ideal T<VAR>f : R →+* S<VAR>g : S →+* T<GOAL>Ideal.comap f (Ideal.comap g I) = Ideal.comap (g.comp f) I
<VAR>R : Type u<VAR>S : Type v<VAR>Semiring R<VAR>Semiring S<VAR>T : Type u_3<VAR>Semiring T<VAR>I : Ideal R<VAR>f : R →+* S<VAR>g : S →+* T<GOAL>Ideal.map g (Ideal.map f I) = Ideal.map (g.comp f) I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>s : Set R<GOAL>Ideal.map f (Ideal.span s) = Ideal.span (⇑f '' s)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>K : Ideal S<GOAL>I ≤ Ideal.comap f K → Ideal.map f I ≤ K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>K : Ideal S<GOAL>Ideal.map f I ≤ K → I ≤ Ideal.comap f K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<GOAL>I ≤ Ideal.comap f (Ideal.map f I)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K : Ideal S<GOAL>Ideal.map f (Ideal.comap f K) ≤ K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<GOAL>Ideal.comap f ⊤ = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal S<GOAL>Ideal.comap f I = ⊤ ↔ I = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<GOAL>Ideal.map f ⊥ = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<GOAL>Ideal.map f (Ideal.comap f (Ideal.map f I)) = Ideal.map f I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K : Ideal S<GOAL>Ideal.comap f (Ideal.map f (Ideal.comap f K)) = Ideal.comap f K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<GOAL>Ideal.map f (I ⊔ J) = Ideal.map f I ⊔ Ideal.map f J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K L : Ideal S<GOAL>Ideal.comap f (K ⊓ L) = Ideal.comap f K ⊓ Ideal.comap f L
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>ι : Sort u_3<VAR>K : ι → Ideal R<GOAL>Ideal.map f (iSup K) = ⨆ i, Ideal.map f (K i)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>ι : Sort u_3<VAR>K : ι → Ideal S<GOAL>Ideal.comap f (iInf K) = ⨅ i, Ideal.comap f (K i)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>s : Set (Ideal R)<GOAL>Ideal.map f (sSup s) = ⨆ I ∈ s, Ideal.map f I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>s : Set (Ideal S)<GOAL>Ideal.comap f (sInf s) = ⨅ I ∈ s, Ideal.comap f I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>s : Set (Ideal S)<GOAL>Ideal.comap f (sInf s) = ⨅ I ∈ Ideal.comap f '' s, I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K : Ideal S<VAR>H : K.IsPrime<GOAL>(Ideal.comap f K).IsPrime
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I J : Ideal R<GOAL>Ideal.map f (I ⊓ J) ≤ Ideal.map f I ⊓ Ideal.map f J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>K L : Ideal S<GOAL>Ideal.comap f K ⊔ Ideal.comap f L ≤ Ideal.comap f (K ⊔ L)
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>r : R<VAR>N : Submodule S M<GOAL>Submodule.restrictScalars R ((algebraMap R S) r • N) = r • Submodule.restrictScalars R N
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>M : Type u_6<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>I : Ideal R<VAR>N : Submodule S M<GOAL>Submodule.restrictScalars R (Ideal.map (algebraMap R S) I • N) = I • Submodule.restrictScalars R N
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>I : Ideal R<GOAL>I • ⊤ = Submodule.restrictScalars R (Ideal.map (algebraMap R S) I)
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>I : Ideal S<GOAL>↑(Submodule.restrictScalars R I) = ↑I
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>Algebra R S<VAR>I J : Ideal S<GOAL>Submodule.restrictScalars R (I * J) = Submodule.restrictScalars R I * Submodule.restrictScalars R J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal S<GOAL>Ideal.map f (Ideal.comap f I) = I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Surjective (Ideal.map f)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Injective (Ideal.comap f)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<GOAL>Ideal.map f (Ideal.comap f I ⊔ Ideal.comap f J) = I ⊔ J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>ι : Sort u_3<VAR>hf : Function.Surjective ⇑f<VAR>K : ι → Ideal S<GOAL>Ideal.map f (⨆ i, Ideal.comap f (K i)) = iSup K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I J : Ideal S<GOAL>Ideal.map f (Ideal.comap f I ⊓ Ideal.comap f J) = I ⊓ J
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>ι : Sort u_3<VAR>hf : Function.Surjective ⇑f<VAR>K : ι → Ideal S<GOAL>Ideal.map f (⨅ i, Ideal.comap f (K i)) = iInf K
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>y : S<VAR>H : y ∈ Ideal.map f I<GOAL>y ∈ ⇑f '' ↑I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>I : Ideal R<VAR>y : S<GOAL>y ∈ Ideal.map f I ↔ ∃ x ∈ I, f x = y
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I : Ideal R<VAR>K : Ideal S<VAR>hf : Function.Surjective ⇑f<GOAL>Ideal.comap f K ≤ I → K ≤ Ideal.map f I