ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>P : R<VAR>hP : P ∉ NonUnitalSubring.closure s<GOAL>P ∉ s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>t : NonUnitalSubring R<GOAL>NonUnitalSubring.closure s ≤ t ↔ s ⊆ ↑t
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s t : Set R<VAR>h : s ⊆ t<GOAL>NonUnitalSubring.closure s ≤ NonUnitalSubring.closure t
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>t : NonUnitalSubring R<VAR>h₁ : s ⊆ ↑t<VAR>h₂ : t ≤ NonUnitalSubring.closure s<GOAL>NonUnitalSubring.closure s = t
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>p : R → Prop<VAR>x : R<VAR>h : x ∈ NonUnitalSubring.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>neg : ∀ (x : R), p x → p (-x)<VAR>mul : ∀ (x y : R), p x → p y → p (x * y)<GOAL>p x
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>p : ↥(NonUnitalSubring.closure s) → Prop<VAR>a : ↥(NonUnitalSubring.closure s)<VAR>mem : ∀ (x : R) (hx : x ∈ s), p ⟨x, ⋯⟩<VAR>zero : p 0<VAR>add : ∀ (x y : ↥(NonUnitalSubring.closure s)), p x → p y → p (x + y)<VAR>neg : ∀ (x : ↥(NonUnitalSubring.closure s)), p x → p (-x)<VAR>mul : ∀ (x y : ↥(NonUnitalSubring.closure s)), p x → p y → p (x * y)<GOAL>p a
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>p : R → R → Prop<VAR>a b : R<VAR>ha : a ∈ NonUnitalSubring.closure s<VAR>hb : b ∈ NonUnitalSubring.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>Hneg_left : ∀ (x y : R), p x y → p (-x) y<VAR>Hneg_right : ∀ (x y : R), p x y → p x (-y)<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 a b
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set R<VAR>x : R<GOAL>x ∈ NonUnitalSubring.closure s ↔ x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<GOAL>NonUnitalSubring.closure ↑s = s
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>NonUnitalSubring.closure ∅ = ⊥
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<GOAL>NonUnitalSubring.closure Set.univ = ⊤
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s t : Set R<GOAL>NonUnitalSubring.closure (s ∪ t) = NonUnitalSubring.closure s ⊔ NonUnitalSubring.closure t
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>ι : Sort u_2<VAR>s : ι → Set R<GOAL>NonUnitalSubring.closure (⋃ i, s i) = ⨆ i, NonUnitalSubring.closure (s i)
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : Set (Set R)<GOAL>NonUnitalSubring.closure (⋃₀ s) = ⨆ t ∈ s, NonUnitalSubring.closure t
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s t : NonUnitalSubring R<VAR>f : F<GOAL>NonUnitalSubring.map f (s ⊔ t) = NonUnitalSubring.map f s ⊔ NonUnitalSubring.map f t
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>ι : Sort u_2<VAR>f : F<VAR>s : ι → NonUnitalSubring R<GOAL>NonUnitalSubring.map f (iSup s) = ⨆ i, NonUnitalSubring.map f (s i)
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>s t : NonUnitalSubring S<VAR>f : F<GOAL>NonUnitalSubring.comap f (s ⊓ t) = NonUnitalSubring.comap f s ⊓ NonUnitalSubring.comap f t
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>ι : Sort u_2<VAR>f : F<VAR>s : ι → NonUnitalSubring S<GOAL>NonUnitalSubring.comap f (iInf s) = ⨅ i, NonUnitalSubring.comap f (s i)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<GOAL>NonUnitalSubring.map f ⊥ = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<GOAL>NonUnitalSubring.comap f ⊤ = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>s : NonUnitalSubring R<VAR>t : NonUnitalSubring S<GOAL>↑(s.prod t) = ↑s ×ˢ ↑t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>s : NonUnitalSubring R<VAR>t : NonUnitalSubring 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>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>s₁ s₂ : NonUnitalSubring R<VAR>hs : s₁ ≤ s₂<VAR>t₁ t₂ : NonUnitalSubring S<VAR>ht : t₁ ≤ t₂<GOAL>s₁.prod t₁ ≤ s₂.prod t₂
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>s : NonUnitalSubring R<GOAL>Monotone fun t => s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>t : NonUnitalSubring S<GOAL>Monotone fun s => s.prod t
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>s : NonUnitalSubring R<GOAL>s.prod ⊤ = NonUnitalSubring.comap (NonUnitalRingHom.fst R S) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>s : NonUnitalSubring S<GOAL>⊤.prod s = NonUnitalSubring.comap (NonUnitalRingHom.snd R S) s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<GOAL>⊤.prod ⊤ = ⊤
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>ι : Sort u_2<VAR>hι : Nonempty ι<VAR>S : ι → NonUnitalSubring 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>NonUnitalNonAssocRing R<VAR>ι : Sort u_2<VAR>Nonempty ι<VAR>S : ι → NonUnitalSubring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<GOAL>↑(⨆ i, S i) = ⋃ i, ↑(S i)
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>S : Set (NonUnitalSubring 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>NonUnitalNonAssocRing R<VAR>S : Set (NonUnitalSubring 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>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R ≃+* S<VAR>K : NonUnitalSubring R<VAR>x : S<GOAL>x ∈ NonUnitalSubring.map (↑f) K ↔ f.symm x ∈ K
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R ≃+* S<VAR>K : NonUnitalSubring R<GOAL>NonUnitalSubring.map (↑f) K = NonUnitalSubring.comap f.symm K
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R ≃+* S<VAR>K : NonUnitalSubring S<GOAL>NonUnitalSubring.comap (↑f) K = NonUnitalSubring.map f.symm K
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<VAR>x : R<GOAL>↑(f.rangeRestrict x) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<GOAL>Function.Surjective ⇑f.rangeRestrict
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<GOAL>f.range = ⊤ ↔ Function.Surjective ⇑f
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<VAR>hf : Function.Surjective ⇑f<GOAL>f.range = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<GOAL>f.eqLocus f = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f g : R →ₙ+* S<VAR>s : Set R<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>Set.EqOn ⇑f ⇑g ↑(NonUnitalSubring.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f g : R →ₙ+* S<VAR>h : Set.EqOn ⇑f ⇑g ↑⊤<GOAL>f = g
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>s : Set R<VAR>hs : NonUnitalSubring.closure s = ⊤<VAR>f g : R →ₙ+* S<VAR>h : Set.EqOn (⇑f) (⇑g) s<GOAL>f = g
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<VAR>s : Set S<GOAL>NonUnitalSubring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubring.comap f (NonUnitalSubring.closure s)
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>f : R →ₙ+* S<VAR>s : Set R<GOAL>NonUnitalSubring.map f (NonUnitalSubring.closure s) = NonUnitalSubring.closure (⇑f '' s)
<VAR>R : Type u<VAR>NonUnitalNonAssocRing R<VAR>s : NonUnitalSubring R<GOAL>(NonUnitalSubringClass.subtype s).range = s
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<GOAL>NonUnitalRingHom.srange (NonUnitalRingHom.fst R S) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<GOAL>NonUnitalRingHom.srange (NonUnitalRingHom.snd R S) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalRing R<VAR>NonUnitalRing S<VAR>g : S → R<VAR>f : R →ₙ+* S<VAR>h : Function.LeftInverse g ⇑f<VAR>x : R<GOAL>↑((RingEquiv.ofLeftInverse' h) x) = f x
<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalRing R<VAR>NonUnitalRing S<VAR>g : S → R<VAR>f : R →ₙ+* S<VAR>h : Function.LeftInverse g ⇑f<VAR>x : ↥f.range<GOAL>(RingEquiv.ofLeftInverse' h).symm x = g ↑x
<VAR>F : Type w<VAR>R : Type u<VAR>S : Type v<VAR>NonUnitalNonAssocRing R<VAR>NonUnitalNonAssocRing S<VAR>FunLike F R S<VAR>NonUnitalRingHomClass F R S<VAR>f : F<VAR>s : Set S<GOAL>NonUnitalSubring.closure (⇑f ⁻¹' s) ≤ NonUnitalSubring.comap f (NonUnitalSubring.closure s)
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>(DirectSum.decompose 𝒜) 1 = 1
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>(DirectSum.decompose 𝒜).symm 1 = 1
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>x y : A<GOAL>(DirectSum.decompose 𝒜) (x * y) = (DirectSum.decompose 𝒜) x * (DirectSum.decompose 𝒜) y
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>x y : ⨁ (i : ι), ↥(𝒜 i)<GOAL>(DirectSum.decompose 𝒜).symm (x * y) = (DirectSum.decompose 𝒜).symm x * (DirectSum.decompose 𝒜).symm y
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>i : ι<VAR>r : A<GOAL>(GradedRing.proj 𝒜 i) r = ↑(((DirectSum.decompose 𝒜) r) i)
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a : ⨁ (i : ι), ↥(𝒜 i)<VAR>i : ι<GOAL>(GradedRing.proj 𝒜 i) ((DirectSum.decompose 𝒜).symm a) = (DirectSum.decompose 𝒜).symm ((DirectSum.of (fun i => ↥(𝒜 i)) i) (a i))
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>(i : ι) → (x : ↥(𝒜 i)) → Decidable (x ≠ 0)<VAR>r : A<VAR>i : ι<GOAL>i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) r) ↔ (GradedRing.proj 𝒜 i) r ≠ 0
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>i j : ι<VAR>AddLeftCancelMonoid ι<VAR>GradedRing 𝒜<VAR>a b : A<VAR>a_mem : a ∈ 𝒜 i<GOAL>↑(((DirectSum.decompose 𝒜) (a * b)) (i + j)) = a * ↑(((DirectSum.decompose 𝒜) b) j)
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>i j : ι<VAR>AddRightCancelMonoid ι<VAR>GradedRing 𝒜<VAR>a b : A<VAR>b_mem : b ∈ 𝒜 j<GOAL>↑(((DirectSum.decompose 𝒜) (a * b)) (i + j)) = ↑(((DirectSum.decompose 𝒜) a) i) * b
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>i j : ι<VAR>AddLeftCancelMonoid ι<VAR>GradedRing 𝒜<VAR>a : ↥(𝒜 i)<VAR>b : A<GOAL>((DirectSum.decompose 𝒜) (↑a * b)) (i + j) = GradedMonoid.GMul.mul a (((DirectSum.decompose 𝒜) b) j)
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>DecidableEq ι<VAR>Semiring A<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>i j : ι<VAR>AddRightCancelMonoid ι<VAR>GradedRing 𝒜<VAR>a : A<VAR>b : ↥(𝒜 j)<GOAL>((DirectSum.decompose 𝒜) (a * ↑b)) (i + j) = GradedMonoid.GMul.mul (((DirectSum.decompose 𝒜) a) i) b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>a : A<GOAL>(DirectSum.decomposeAlgEquiv 𝒜) a = (DirectSum.decompose 𝒜) a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>a : ⨁ (i : ι), ↥(𝒜 i)<GOAL>(DirectSum.decomposeAlgEquiv 𝒜).symm a = (DirectSum.decompose 𝒜).symm a
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>r : R<GOAL>(DirectSum.decompose 𝒜) ((algebraMap R A) r) = (algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>r : R<GOAL>(DirectSum.decompose 𝒜).symm ((algebraMap R (⨁ (i : ι), ↥(𝒜 i))) r) = (algebraMap R A) r
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>i : ι<VAR>r : A<GOAL>(GradedAlgebra.proj 𝒜 i) r = ↑(((DirectSum.decompose 𝒜) r) i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>a : ⨁ (i : ι), ↥(𝒜 i)<VAR>i : ι<GOAL>(GradedAlgebra.proj 𝒜 i) ((DirectSum.decompose 𝒜).symm a) = (DirectSum.decompose 𝒜).symm ((DirectSum.of (fun i => ↥(𝒜 i)) i) (a i))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>DecidableEq ι<VAR>AddMonoid ι<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>DecidableEq A<VAR>r : A<VAR>i : ι<GOAL>i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) r) ↔ (GradedAlgebra.proj 𝒜 i) r ≠ 0
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a : A<GOAL>(GradedRing.projZeroRingHom 𝒜) a = ↑(((DirectSum.decompose 𝒜) a) 0)
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a : A<GOAL>↑((GradedRing.projZeroRingHom' 𝒜) a) = (GradedRing.projZeroRingHom 𝒜) a
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a : ↥(𝒜 0)<GOAL>(GradedRing.projZeroRingHom' 𝒜) ↑a = a
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<GOAL>Function.Surjective ⇑(GradedRing.projZeroRingHom' 𝒜)
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a b : A<VAR>n i : ι<VAR>a_mem : a ∈ 𝒜 i<VAR>h : ¬i ≤ n<GOAL>↑(((DirectSum.decompose 𝒜) (a * b)) n) = 0
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a b : A<VAR>n i : ι<VAR>b_mem : b ∈ 𝒜 i<VAR>h : ¬i ≤ n<GOAL>↑(((DirectSum.decompose 𝒜) (a * b)) n) = 0
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a b : A<VAR>n i : ι<VAR>Sub ι<VAR>OrderedSub ι<VAR>ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>a_mem : a ∈ 𝒜 i<VAR>h : i ≤ n<GOAL>↑(((DirectSum.decompose 𝒜) (a * b)) n) = a * ↑(((DirectSum.decompose 𝒜) b) (n - i))
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a b : A<VAR>n i : ι<VAR>Sub ι<VAR>OrderedSub ι<VAR>ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>b_mem : b ∈ 𝒜 i<VAR>h : i ≤ n<GOAL>↑(((DirectSum.decompose 𝒜) (a * b)) n) = ↑(((DirectSum.decompose 𝒜) a) (n - i)) * b
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a b : A<VAR>i : ι<VAR>Sub ι<VAR>OrderedSub ι<VAR>ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : ι<VAR>Decidable (i ≤ n)<VAR>a_mem : a ∈ 𝒜 i<GOAL>↑(((DirectSum.decompose 𝒜) (a * b)) n) = if i ≤ n then a * ↑(((DirectSum.decompose 𝒜) b) (n - i)) else 0
<VAR>ι : Type u_1<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>Semiring A<VAR>DecidableEq ι<VAR>CanonicallyOrderedAddCommMonoid ι<VAR>SetLike σ A<VAR>AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>GradedRing 𝒜<VAR>a b : A<VAR>i : ι<VAR>Sub ι<VAR>OrderedSub ι<VAR>ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : ι<VAR>Decidable (i ≤ n)<VAR>b_mem : b ∈ 𝒜 i<GOAL>↑(((DirectSum.decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(((DirectSum.decompose 𝒜) a) (n - i)) * b else 0
<VAR>R : Type u_3<VAR>S : Type u_2<VAR>M : Type u_4<VAR>N : Type u_1<VAR>Semiring R<VAR>Semiring S<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module S N<VAR>e : M ≃ₛₗ[σ] N<VAR>r : R<GOAL>IsSMulRegular M r ↔ IsSMulRegular N (σ r)
<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_1<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>e : M ≃ₗ[R] N<VAR>r : R<GOAL>IsSMulRegular M r ↔ IsSMulRegular N r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<VAR>h : IsSMulRegular M r<GOAL>IsSMulRegular (↥N) r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>Module.Flat R M<VAR>r : R<VAR>h : IsSMulRegular M' r<GOAL>IsSMulRegular (TensorProduct R M M') r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>CommRing R<VAR>AddCommGroup M<VAR>AddCommGroup M'<VAR>Module R M<VAR>Module R M'<VAR>Module.Flat R M<VAR>r : R<VAR>h : IsSMulRegular M' r<GOAL>IsSMulRegular (TensorProduct R M' M) r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>CommSemiring R<VAR>Semiring S<VAR>Algebra R S<VAR>AddCommMonoid M<VAR>Module R M<VAR>Module S M<VAR>IsScalarTower R S M<VAR>r : R<GOAL>IsSMulRegular M ((algebraMap R S) r) ↔ IsSMulRegular M r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>IsSMulRegular M r ↔ ∀ (x : M), r • x = 0 → x = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>IsSMulRegular M r ↔ r ∈ nonZeroSMulDivisors R M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>h : ∀ (x : M), r • x = 0 → x = 0<GOAL>IsSMulRegular M r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>IsSMulRegular (↥N) r ↔ ∀ x ∈ N, r • x = 0 → x = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>IsSMulRegular (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N → x ∈ N
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<VAR>h1 : IsSMulRegular (M ⧸ N) r<VAR>x : M<VAR>h2 : r • x ∈ N<GOAL>x ∈ N
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>AddCommGroup M''<VAR>Module R M''<VAR>r : R<VAR>f : M →ₗ[R] M'<VAR>g : M' →ₗ[R] M''<VAR>hf : Function.Injective ⇑f<VAR>hfg : LinearMap.range f = LinearMap.ker g<VAR>h1 : IsSMulRegular M r<VAR>h2 : IsSMulRegular M'' r<GOAL>IsSMulRegular M' r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<VAR>h1 : IsSMulRegular (↥N) r<VAR>h2 : IsSMulRegular (M ⧸ N) r<GOAL>IsSMulRegular M r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>IsNoetherianRing R<GOAL>⋃ p ∈ associatedPrimes R M, ↑p = {r | IsSMulRegular M r}ᶜ
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<GOAL>IsSMulRegular M r ↔ LinearMap.ker ((LinearMap.lsmul R M) r) = ⊥
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>IsSMulRegular (↥N) r ↔ Disjoint (LinearMap.ker ((LinearMap.lsmul R M) r)) N
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>IsSMulRegular (M ⧸ N) r ↔ Submodule.comap ((LinearMap.lsmul R M) r) N ≤ N
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>IsSMulRegular (M ⧸ N) r ↔ Submodule.comap ((LinearMap.lsmul R M) r) N = N
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>IsSMulRegular M r → (IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>r : R<VAR>h : LinearMap.ker ((LinearMap.lsmul R M) r) = ⊥<GOAL>IsSMulRegular M r
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>N : Submodule R M<VAR>r : R<GOAL>IsSMulRegular (M ⧸ N) r → r • ⊤ ⊓ N ≤ r • N
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>M' : Type u_4<VAR>M'' : Type u_5<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>AddCommGroup M'<VAR>Module R M'<VAR>AddCommGroup M''<VAR>Module R M''<VAR>M''' : Type u_6<VAR>AddCommGroup M'''<VAR>Module R M'''<VAR>r : R<VAR>f₁ : M →ₗ[R] M'<VAR>f₂ : M' →ₗ[R] M''<VAR>f₃ : M'' →ₗ[R] M'''<VAR>h₁₂ : Function.Exact ⇑f₁ ⇑f₂<VAR>h₂₃ : Function.Exact ⇑f₂ ⇑f₃<VAR>h : IsSMulRegular M''' r<GOAL>Function.Exact ⇑((QuotSMulTop.map r) f₁) ⇑((QuotSMulTop.map r) f₂)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>CommRing A<VAR>CommRing B<VAR>Algebra A B<VAR>Module.Free A B<VAR>Module.Finite A B<VAR>a : A<VAR>x : B<GOAL>∃ r, (Algebra.norm A) (1 + a • x) = 1 + (Algebra.trace A B) x * a + r * a ^ 2
<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>hI : Ideal.IsHomogeneous 𝒜 I<VAR>x : A<GOAL>x ∈ I ↔ ∀ (i : ι), ↑(((DirectSum.decompose 𝒜) x) 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>self : HomogeneousIdeal 𝒜<GOAL>Ideal.IsHomogeneous 𝒜 self.toSubmodule
<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.IsHomogeneous 𝒜 I.toIdeal