ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<GOAL>Function.Injective HomogeneousIdeal.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I J : HomogeneousIdeal 𝒜<VAR>h : I.toIdeal = J.toIdeal<GOAL>I = J
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I J : HomogeneousIdeal 𝒜<VAR>h : ∀ (i : ι), ∀ x ∈ 𝒜 i, x ∈ I ↔ x ∈ J<GOAL>I = J
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : HomogeneousIdeal 𝒜<VAR>x : A<GOAL>x ∈ I.toIdeal ↔ x ∈ I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>𝒜 : ι → σ<GOAL>Monotone (Ideal.homogeneousCore' 𝒜)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>𝒜 : ι → σ<VAR>I : Ideal A<GOAL>Ideal.homogeneousCore' 𝒜 I ≤ I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>Ideal.IsHomogeneous 𝒜 I ↔ ∀ (i : ι), ↑I ⊆ ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>Ideal.IsHomogeneous 𝒜 I ↔ ↑I ⊆ ⋂ i, ⇑(GradedRing.proj 𝒜 i) ⁻¹' ↑I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>r x : A<VAR>hx₁ : SetLike.Homogeneous 𝒜 x<VAR>hx₂ : x ∈ I<VAR>j : ι<GOAL>(GradedRing.proj 𝒜 j) (r * x) ∈ I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>s : Set A<VAR>h : ∀ x ∈ s, SetLike.Homogeneous 𝒜 x<GOAL>Ideal.IsHomogeneous 𝒜 (Ideal.span s)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<GOAL>Monotone (Ideal.homogeneousCore 𝒜)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>(Ideal.homogeneousCore 𝒜 I).toIdeal ≤ I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>x : A<VAR>h : SetLike.Homogeneous 𝒜 x<VAR>hmem : x ∈ I<GOAL>x ∈ Ideal.homogeneousCore 𝒜 I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>h : Ideal.IsHomogeneous 𝒜 I<GOAL>(Ideal.homogeneousCore 𝒜 I).toIdeal = I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : HomogeneousIdeal 𝒜<GOAL>Ideal.homogeneousCore 𝒜 I.toIdeal = I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>Ideal.IsHomogeneous 𝒜 I ↔ (Ideal.homogeneousCore 𝒜 I).toIdeal = I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>Ideal.IsHomogeneous 𝒜 I ↔ ∃ S, I = Ideal.span (Subtype.val '' S)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>Ideal.IsHomogeneous 𝒜 ⊥
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>Ideal.IsHomogeneous 𝒜 ⊤
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : Ideal A<VAR>HI : Ideal.IsHomogeneous 𝒜 I<VAR>HJ : Ideal.IsHomogeneous 𝒜 J<GOAL>Ideal.IsHomogeneous 𝒜 (I ⊓ J)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : Ideal A<VAR>HI : Ideal.IsHomogeneous 𝒜 I<VAR>HJ : Ideal.IsHomogeneous 𝒜 J<GOAL>Ideal.IsHomogeneous 𝒜 (I ⊔ J)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>h : ∀ (i : κ), Ideal.IsHomogeneous 𝒜 (f i)<GOAL>Ideal.IsHomogeneous 𝒜 (⨆ i, f i)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>κ : Sort u_5<VAR>f : κ → Ideal A<VAR>h : ∀ (i : κ), Ideal.IsHomogeneous 𝒜 (f i)<GOAL>Ideal.IsHomogeneous 𝒜 (⨅ i, f i)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>κ : Sort u_5<VAR>κ' : κ → Sort u_6<VAR>f : (i : κ) → κ' i → Ideal A<VAR>h : ∀ (i : κ) (j : κ' i), Ideal.IsHomogeneous 𝒜 (f i j)<GOAL>Ideal.IsHomogeneous 𝒜 (⨆ i, ⨆ j, f i j)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>κ : Sort u_5<VAR>κ' : κ → Sort u_6<VAR>f : (i : κ) → κ' i → Ideal A<VAR>h : ∀ (i : κ) (j : κ' i), Ideal.IsHomogeneous 𝒜 (f i j)<GOAL>Ideal.IsHomogeneous 𝒜 (⨅ i, ⨅ j, f i j)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>ℐ : Set (Ideal A)<VAR>h : ∀ I ∈ ℐ, Ideal.IsHomogeneous 𝒜 I<GOAL>Ideal.IsHomogeneous 𝒜 (sSup ℐ)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>ℐ : Set (Ideal A)<VAR>h : ∀ I ∈ ℐ, Ideal.IsHomogeneous 𝒜 I<GOAL>Ideal.IsHomogeneous 𝒜 (sInf ℐ)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>↑⊤ = Set.univ
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>↑⊥ = 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : HomogeneousIdeal 𝒜<GOAL>↑(I ⊔ J) = ↑I + ↑J
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : HomogeneousIdeal 𝒜<GOAL>↑(I ⊓ J) = ↑I ∩ ↑J
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>⊤.toIdeal = ⊤
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>⊥.toIdeal = ⊥
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : HomogeneousIdeal 𝒜<GOAL>(I ⊔ J).toIdeal = I.toIdeal ⊔ J.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : HomogeneousIdeal 𝒜<GOAL>(I ⊓ J).toIdeal = I.toIdeal ⊓ J.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>ℐ : Set (HomogeneousIdeal 𝒜)<GOAL>(sSup ℐ).toIdeal = ⨆ s ∈ ℐ, s.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>ℐ : Set (HomogeneousIdeal 𝒜)<GOAL>(sInf ℐ).toIdeal = ⨅ s ∈ ℐ, s.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>κ : Sort u_5<VAR>s : κ → HomogeneousIdeal 𝒜<GOAL>(⨆ i, s i).toIdeal = ⨆ i, (s i).toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>κ : Sort u_5<VAR>s : κ → HomogeneousIdeal 𝒜<GOAL>(⨅ i, s i).toIdeal = ⨅ i, (s i).toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>κ : Sort u_5<VAR>κ' : κ → Sort u_6<VAR>s : (i : κ) → κ' i → HomogeneousIdeal 𝒜<GOAL>(⨆ i, ⨆ j, s i j).toIdeal = ⨆ i, ⨆ j, (s i j).toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>κ : Sort u_5<VAR>κ' : κ → Sort u_6<VAR>s : (i : κ) → κ' i → HomogeneousIdeal 𝒜<GOAL>(⨅ i, ⨅ j, s i j).toIdeal = ⨅ i, ⨅ j, (s i j).toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : HomogeneousIdeal 𝒜<GOAL>I = ⊤ ↔ I.toIdeal = ⊤
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : HomogeneousIdeal 𝒜<GOAL>I = ⊥ ↔ I.toIdeal = ⊥
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : HomogeneousIdeal 𝒜<GOAL>(I + J).toIdeal = I.toIdeal + J.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>CommSemiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : Ideal A<VAR>HI : Ideal.IsHomogeneous 𝒜 I<VAR>HJ : Ideal.IsHomogeneous 𝒜 J<GOAL>Ideal.IsHomogeneous 𝒜 (I * J)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>CommSemiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I J : HomogeneousIdeal 𝒜<GOAL>(I * J).toIdeal = I.toIdeal * J.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>GaloisConnection HomogeneousIdeal.toIdeal (Ideal.homogeneousCore 𝒜)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>Ideal.homogeneousCore 𝒜 I = sSup {J | J.toIdeal ≤ I}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>Ideal.homogeneousCore' 𝒜 I = sSup {J | Ideal.IsHomogeneous 𝒜 J ∧ J ≤ I}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>I ≤ (Ideal.homogeneousHull 𝒜 I).toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>Monotone (Ideal.homogeneousHull 𝒜)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>h : Ideal.IsHomogeneous 𝒜 I<GOAL>(Ideal.homogeneousHull 𝒜 I).toIdeal = I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : HomogeneousIdeal 𝒜<GOAL>Ideal.homogeneousHull 𝒜 I.toIdeal = I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>(Ideal.homogeneousHull 𝒜 I).toIdeal = ⨆ i, Ideal.span (⇑(GradedRing.proj 𝒜 i) '' ↑I)
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>Ideal.homogeneousHull 𝒜 I = ⨆ i, { toSubmodule := Ideal.span (⇑(GradedRing.proj 𝒜 i) '' ↑I), is_homogeneous' := ⋯ }
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>GaloisConnection (Ideal.homogeneousHull 𝒜) HomogeneousIdeal.toIdeal
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<GOAL>Ideal.homogeneousHull 𝒜 I = sInf {J | I ≤ J.toIdeal}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a : A<GOAL>a ∈ HomogeneousIdeal.irrelevant 𝒜 ↔ (GradedRing.proj 𝒜 0) a = 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>(HomogeneousIdeal.irrelevant 𝒜).toIdeal = RingHom.ker (GradedRing.projZeroRingHom 𝒜)
<VAR>R : Type u<VAR>A : Type w<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>b : Basis ι R M<VAR>h : Function.Bijective ⇑(algebraMap R A)<GOAL>∀ (a : M) (a_1 : ι), ((Basis.algebraMapCoeffs A b h).repr a) a_1 = (algebraMap R A) ((b.repr a) a_1)
<VAR>R : Type u<VAR>A : Type w<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>b : Basis ι R M<VAR>h : Function.Bijective ⇑(algebraMap R A)<GOAL>∀ (a : M), ((Basis.algebraMapCoeffs A b h).repr a).support.val = Multiset.filter (fun x => ¬(RingEquiv.ofBijective (algebraMap R A) h).symm.symm ((b.repr a) x) = 0) (b.repr a).support.val
<VAR>R : Type u<VAR>A : Type w<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>b : Basis ι R M<VAR>h : Function.Bijective ⇑(algebraMap R A)<VAR>i : ι<GOAL>(Basis.algebraMapCoeffs A b h) i = b i
<VAR>R : Type u<VAR>A : Type w<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>AddCommMonoid M<VAR>Algebra R A<VAR>Module A M<VAR>Module R M<VAR>IsScalarTower R A M<VAR>b : Basis ι R M<VAR>h : Function.Bijective ⇑(algebraMap R A)<GOAL>⇑(Basis.algebraMapCoeffs A b h) = ⇑b
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>ι : Type v₁<VAR>b : ι → S<VAR>ι' : Type w₁<VAR>c : ι' → A<VAR>hb : LinearIndependent R b<VAR>hc : LinearIndependent S c<GOAL>LinearIndependent R fun p => b p.1 • c p.2
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>ι : Type u_1<VAR>Nonempty ι<VAR>b : Basis ι S A<GOAL>IsScalarTower R S S
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>ι : Type u_1<VAR>b : Basis ι S A<GOAL>IsScalarTower R S (ι →₀ S)
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>ι : Type v₁<VAR>ι' : Type w₁<VAR>b : Basis ι R S<VAR>c : Basis ι' S A<VAR>x : A<VAR>ij : ι × ι'<GOAL>((b.smulTower c).repr x) ij = (b.repr ((c.repr x) ij.2)) ij.1
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>ι : Type v₁<VAR>ι' : Type w₁<VAR>b : Basis ι R S<VAR>c : Basis ι' S A<VAR>x : A<VAR>i : ι<VAR>j : ι'<GOAL>((b.smulTower c).repr x) (i, j) = (b.repr ((c.repr x) j)) i
<VAR>R : Type u<VAR>S : Type v<VAR>A : Type w<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid A<VAR>Module R S<VAR>Module S A<VAR>Module R A<VAR>IsScalarTower R S A<VAR>ι : Type v₁<VAR>ι' : Type w₁<VAR>b : Basis ι R S<VAR>c : Basis ι' S A<VAR>ij : ι × ι'<GOAL>(b.smulTower c) ij = b ij.1 • c ij.2
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>Ring S<VAR>Algebra R S<VAR>ι : Type u_1<VAR>NoZeroDivisors R<VAR>Nontrivial S<VAR>b : Basis ι R S<GOAL>Function.Injective ⇑(algebraMap R S)
<VAR>α : Type u<GOAL>Function.Injective FreeCommRing.of
<VAR>α : Type u<VAR>a : α<VAR>m : Multiset α<GOAL>FreeAbelianGroup.of (Multiplicative.ofAdd (a ::ₘ m)) = FreeCommRing.of a * FreeAbelianGroup.of (Multiplicative.ofAdd m)
<VAR>α : Type u<VAR>C : FreeCommRing α → Prop<VAR>z : FreeCommRing α<VAR>hn1 : C (-1)<VAR>hb : ∀ (b : α), C (FreeCommRing.of b)<VAR>ha : ∀ (x y : FreeCommRing α), C x → C y → C (x + y)<VAR>hm : ∀ (x y : FreeCommRing α), C x → C y → C (x * y)<GOAL>C z
<VAR>α : Type u<VAR>R : Type v<VAR>CommRing R<VAR>f : α → R<VAR>x : α<GOAL>(FreeCommRing.lift f) (FreeCommRing.of x) = f x
<VAR>α : Type u<VAR>R : Type v<VAR>CommRing R<VAR>f : FreeCommRing α →+* R<GOAL>FreeCommRing.lift (⇑f ∘ FreeCommRing.of) = f
<VAR>α : Type u<VAR>R : Type v<VAR>CommRing R<VAR>f g : FreeCommRing α →+* R<VAR>h : ∀ (x : α), f (FreeCommRing.of x) = g (FreeCommRing.of x)<GOAL>f = g
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<GOAL>(FreeCommRing.map f) (FreeCommRing.of x) = FreeCommRing.of (f x)
<VAR>α : Type u<VAR>x : FreeCommRing α<VAR>s t : Set α<VAR>hs : x.IsSupported s<VAR>hst : s ⊆ t<GOAL>x.IsSupported t
<VAR>α : Type u<VAR>x y : FreeCommRing α<VAR>s : Set α<VAR>hxs : x.IsSupported s<VAR>hys : y.IsSupported s<GOAL>(x + y).IsSupported s
<VAR>α : Type u<VAR>x : FreeCommRing α<VAR>s : Set α<VAR>hxs : x.IsSupported s<GOAL>(-x).IsSupported s
<VAR>α : Type u<VAR>x y : FreeCommRing α<VAR>s : Set α<VAR>hxs : x.IsSupported s<VAR>hys : y.IsSupported s<GOAL>(x - y).IsSupported s
<VAR>α : Type u<VAR>x y : FreeCommRing α<VAR>s : Set α<VAR>hxs : x.IsSupported s<VAR>hys : y.IsSupported s<GOAL>(x * y).IsSupported s
<VAR>α : Type u<VAR>s : Set α<GOAL>FreeCommRing.IsSupported 0 s
<VAR>α : Type u<VAR>s : Set α<GOAL>FreeCommRing.IsSupported 1 s
<VAR>α : Type u<VAR>i : ℤ<VAR>s : Set α<GOAL>(↑i).IsSupported s
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>p : α<GOAL>(FreeCommRing.restriction s) (FreeCommRing.of p) = if H : p ∈ s then FreeCommRing.of ⟨p, H⟩ else 0
<VAR>α : Type u<VAR>p : α<VAR>s : Set α<GOAL>(FreeCommRing.of p).IsSupported s ↔ p ∈ s
<VAR>α : Type u<VAR>x : FreeCommRing α<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>hxs : x.IsSupported s<GOAL>(FreeCommRing.map Subtype.val) ((FreeCommRing.restriction s) x) = x
<VAR>α : Type u<VAR>x : FreeCommRing α<GOAL>∃ s, s.Finite ∧ x.IsSupported s
<VAR>α : Type u<VAR>x : FreeCommRing α<GOAL>∃ s, x.IsSupported ↑s
<VAR>α : Type u<VAR>a : α<GOAL>↑(FreeRing.of a) = FreeCommRing.of a
<VAR>α : Type u<VAR>x y : FreeRing α<GOAL>↑(x + y) = ↑x + ↑y
<VAR>α : Type u<VAR>x y : FreeRing α<GOAL>↑(x * y) = ↑x * ↑y
<VAR>α : Type u<GOAL>Function.Surjective FreeRing.castFreeCommRing
<VAR>α : Type u<GOAL>FreeRing.castFreeCommRing = Functor.map fun l => ↑l
<VAR>R : Type u_1<VAR>CommRing R<VAR>r : R<GOAL>IsLocalization.Away r (AdjoinRoot (Polynomial.C r * Polynomial.X - 1))
<VAR>R : Type u_1<VAR>CommRing R<VAR>r : R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization.Away r S<GOAL>Algebra.FinitePresentation R S
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>CommRing A<VAR>LinearOrderedCancelAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>hI : Ideal.IsHomogeneous 𝒜 I<VAR>I_ne_top : I ≠ ⊤<VAR>homogeneous_mem_or_mem : ∀ {x y : A}, SetLike.Homogeneous 𝒜 x → SetLike.Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I<GOAL>I.IsPrime
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>CommRing A<VAR>LinearOrderedCancelAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>h : Ideal.IsHomogeneous 𝒜 I<GOAL>I.IsPrime ↔ I ≠ ⊤ ∧ ∀ {x y : A}, SetLike.Homogeneous 𝒜 x → SetLike.Homogeneous 𝒜 y → x * y ∈ I → x ∈ I ∨ y ∈ I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>CommRing A<VAR>LinearOrderedCancelAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>h : I.IsPrime<GOAL>(Ideal.homogeneousCore 𝒜 I).toIdeal.IsPrime
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>CommRing A<VAR>LinearOrderedCancelAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>hI : Ideal.IsHomogeneous 𝒜 I<GOAL>I.radical = sInf {J | Ideal.IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>CommRing A<VAR>LinearOrderedCancelAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : Ideal A<VAR>h : Ideal.IsHomogeneous 𝒜 I<GOAL>Ideal.IsHomogeneous 𝒜 I.radical
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>CommRing A<VAR>LinearOrderedCancelAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>I : HomogeneousIdeal 𝒜<GOAL>I.radical.toIdeal = I.toIdeal.radical
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<GOAL>IsLocalization.IsInteger R 0
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<GOAL>IsLocalization.IsInteger R 1
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>a b : S<VAR>ha : IsLocalization.IsInteger R a<VAR>hb : IsLocalization.IsInteger R b<GOAL>IsLocalization.IsInteger R (a + b)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>a b : S<VAR>ha : IsLocalization.IsInteger R a<VAR>hb : IsLocalization.IsInteger R b<GOAL>IsLocalization.IsInteger R (a * b)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>a : R<VAR>b : S<VAR>hb : IsLocalization.IsInteger R b<GOAL>IsLocalization.IsInteger R (a • b)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>a : S<GOAL>∃ b, IsLocalization.IsInteger R (a * (algebraMap R S) ↑b)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>a : S<GOAL>∃ b, IsLocalization.IsInteger R (↑b • a)