ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>hdeg : c1.deg = c2.deg<VAR>hnum : ↑c1.num = ↑c2.num<VAR>hden : ↑c1.den = ↑c2.den<GOAL>c1 = c2
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>HomogeneousLocalization.NumDenSameDeg.deg 1 = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>↑(HomogeneousLocalization.NumDenSameDeg.num 1) = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>↑(HomogeneousLocalization.NumDenSameDeg.den 1) = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>HomogeneousLocalization.NumDenSameDeg.deg 0 = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>HomogeneousLocalization.NumDenSameDeg.num 0 = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>↑(HomogeneousLocalization.NumDenSameDeg.den 0) = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>(c1 * c2).deg = c1.deg + c2.deg
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>↑(c1 * c2).num = ↑c1.num * ↑c2.num
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>↑(c1 * c2).den = ↑c1.den * ↑c2.den
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>(c1 + c2).deg = c1.deg + c2.deg
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>↑(c1 + c2).num = ↑c1.den * ↑c2.num + ↑c2.den * ↑c1.num
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c1 c2 : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>↑(c1 + c2).den = ↑c1.den * ↑c2.den
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>(-c).deg = c.deg
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>↑(-c).num = -↑c.num
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>↑(-c).den = ↑c.den
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>n : ℕ<GOAL>(c ^ n).deg = n • c.deg
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>n : ℕ<GOAL>↑(c ^ n).num = ↑c.num ^ n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>n : ℕ<GOAL>↑(c ^ n).den = ↑c.den ^ n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>SMul α R<VAR>SMul α A<VAR>IsScalarTower α R A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>m : α<GOAL>(m • c).deg = c.deg
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>SMul α R<VAR>SMul α A<VAR>IsScalarTower α R A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>m : α<GOAL>↑(m • c).num = m • ↑c.num
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>SMul α R<VAR>SMul α A<VAR>IsScalarTower α R A<VAR>c : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>m : α<GOAL>↑(m • c).den = ↑c.den
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<GOAL>Function.Surjective HomogeneousLocalization.mk
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>i : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>(HomogeneousLocalization.mk i).val = Localization.mk ↑i.num ⟨↑i.den, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<GOAL>Function.Injective HomogeneousLocalization.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>hx : 0 ∈ x<GOAL>Subsingleton (HomogeneousLocalization 𝒜 x)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>i : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>n : ℕ<GOAL>HomogeneousLocalization.mk (i ^ n) = HomogeneousLocalization.mk i ^ n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>SMul α R<VAR>SMul α A<VAR>IsScalarTower α R A<VAR>IsScalarTower α A A<VAR>i : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>m : α<GOAL>HomogeneousLocalization.mk (m • i) = m • HomogeneousLocalization.mk i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>SMul α R<VAR>SMul α A<VAR>IsScalarTower α R A<VAR>IsScalarTower α A A<VAR>n : α<VAR>y : HomogeneousLocalization 𝒜 x<GOAL>(n • y).val = n • y.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>n : ℕ<VAR>y : HomogeneousLocalization 𝒜 x<GOAL>(n • y).val = n • y.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>n : ℤ<VAR>y : HomogeneousLocalization 𝒜 x<GOAL>(n • y).val = n • y.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>i : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>HomogeneousLocalization.mk (-i) = -HomogeneousLocalization.mk i
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>i j : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>HomogeneousLocalization.mk (i + j) = HomogeneousLocalization.mk i + HomogeneousLocalization.mk j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>i j : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>HomogeneousLocalization.mk (i * j) = HomogeneousLocalization.mk i * HomogeneousLocalization.mk j
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>HomogeneousLocalization.mk 1 = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>HomogeneousLocalization.mk 0 = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>0 = Quotient.mk'' 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>1 = Quotient.mk'' 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>HomogeneousLocalization.val 0 = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<GOAL>HomogeneousLocalization.val 1 = 1
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : HomogeneousLocalization 𝒜 x<GOAL>(y1 + y2).val = y1.val + y2.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : HomogeneousLocalization 𝒜 x<GOAL>(y1 * y2).val = y1.val * y2.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>y : HomogeneousLocalization 𝒜 x<GOAL>(-y).val = -y.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y1 y2 : HomogeneousLocalization 𝒜 x<GOAL>(y1 - y2).val = y1.val - y2.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y : HomogeneousLocalization 𝒜 x<VAR>n : ℕ<GOAL>(y ^ n).val = y.val ^ n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>n : ℕ<GOAL>(↑n).val = ↑n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>n : ℤ<GOAL>(↑n).val = ↑n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>y : HomogeneousLocalization 𝒜 x<GOAL>(algebraMap (HomogeneousLocalization 𝒜 x) (at x)) y = y.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>h : f.num = 0<GOAL>HomogeneousLocalization.mk f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization.NumDenSameDeg 𝒜 x<VAR>h : f.den = 0<GOAL>HomogeneousLocalization.mk f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization 𝒜 x<GOAL>f.den ∈ x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization 𝒜 x<GOAL>f.num ∈ 𝒜 f.deg
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization 𝒜 x<GOAL>f.den ∈ 𝒜 f.deg
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization 𝒜 x<GOAL>f.val = Localization.mk f.num ⟨f.den, ⋯⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization 𝒜 x<GOAL>f.den • f.val = (algebraMap A (at x)) f.num
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>x : Submonoid A<VAR>f g : HomogeneousLocalization 𝒜 x<GOAL>f = g ↔ f.val = g.val
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>𝔭 : Ideal A<VAR>𝔭.IsPrime<VAR>f : HomogeneousLocalization.AtPrime 𝒜 𝔭<GOAL>IsUnit (HomogeneousLocalization.val f) ↔ IsUnit f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : HomogeneousLocalization.Away 𝒜 f<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, f ^ n • HomogeneousLocalization.val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>AddCommMonoid ι<VAR>DecidableEq ι<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>GradedAlgebra 𝒜<VAR>B : Type u_4<VAR>CommRing B<VAR>Algebra R B<VAR>ℬ : ι → Submodule R B<VAR>GradedAlgebra ℬ<VAR>P : Submonoid A<VAR>Q : Submonoid B<VAR>g : A →+* B<VAR>comap_le : P ≤ Submonoid.comap g Q<VAR>hg : ∀ (i : ι), ∀ a ∈ 𝒜 i, g a ∈ ℬ i<VAR>x : HomogeneousLocalization.NumDenSameDeg 𝒜 P<GOAL>(HomogeneousLocalization.map 𝒜 ℬ g comap_le hg) (HomogeneousLocalization.mk x) = HomogeneousLocalization.mk { deg := x.deg, num := ⟨g ↑x.num, ⋯⟩, den := ⟨g ↑x.den, ⋯⟩, den_mem := ⋯ }
<VAR>R : Type u_1<VAR>Ring R<VAR>x : R<VAR>n : ℕ<VAR>hx : (x - x ^ 2) ^ n = 0<GOAL>IsIdempotentElem (1 - (1 - x ^ n) ^ n)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₁ : S<VAR>he : e₁ ∈ f.range<VAR>he₁ : IsIdempotentElem e₁<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>he₁e₂ : e₁ * f e₂ = 0<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e₁ : S<VAR>he : e₁ ∈ f.range<VAR>he₁ : IsIdempotentElem e₁<VAR>e₂ : R<VAR>he₂ : IsIdempotentElem e₂<VAR>he₁e₂ : e₁ * f e₂ = 0<VAR>he₂e₁ : f e₂ * e₁ = 0<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : S<VAR>he : e ∈ f.range<VAR>he' : IsIdempotentElem e<GOAL>∃ e', IsIdempotentElem e' ∧ f e' = e
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<GOAL>OrthogonalIdempotents e ↔ (∀ (i : I), IsIdempotentElem (e i)) ∧ ∀ (i j : I), i ≠ j → e i * e j = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>self : OrthogonalIdempotents e<VAR>i : I<GOAL>IsIdempotentElem (e i)
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>self : OrthogonalIdempotents e<VAR>i j : I<GOAL>i ≠ j → e i * e j = 0
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>DecidableEq I<VAR>he : OrthogonalIdempotents e<VAR>i j : I<GOAL>e i * e j = if i = j then e i else 0
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>DecidableEq I<GOAL>OrthogonalIdempotents e ↔ ∀ (i j : I), e i * e j = if i = j then e i else 0
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>Fintype I<GOAL>IsIdempotentElem (∑ i : I, e i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<GOAL>OrthogonalIdempotents (⇑f ∘ e)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>hf : Function.Injective ⇑f<GOAL>OrthogonalIdempotents (⇑f ∘ e) ↔ OrthogonalIdempotents e
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>J : Type u_4<VAR>i : J ↪ I<GOAL>OrthogonalIdempotents (e ∘ ⇑i)
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>J : Type u_4<VAR>i : J ≃ I<GOAL>OrthogonalIdempotents (e ∘ ⇑i) ↔ OrthogonalIdempotents e
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>Unique I<GOAL>OrthogonalIdempotents e ↔ IsIdempotentElem (e default)
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>Fintype I<VAR>x : R<VAR>hx : IsIdempotentElem x<VAR>hx₁ : x * ∑ i : I, e i = 0<VAR>hx₂ : (∑ i : I, e i) * x = 0<GOAL>OrthogonalIdempotents fun x_1 => x_1.elim x e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>n : ℕ<VAR>e : Fin n → S<VAR>he : OrthogonalIdempotents e<VAR>he' : ∀ (i : Fin n), e i ∈ f.range<GOAL>∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>Finite I<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : I → S<VAR>he : OrthogonalIdempotents e<VAR>he' : ∀ (i : I), e i ∈ f.range<GOAL>∃ e', OrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<GOAL>CompleteOrthogonalIdempotents e ↔ OrthogonalIdempotents e ∧ ∑ i : I, e i = 1
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<VAR>self : CompleteOrthogonalIdempotents e<GOAL>∑ i : I, e i = 1
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>Fintype I<VAR>Unique I<GOAL>CompleteOrthogonalIdempotents e ↔ e default = 1
<VAR>R : Type u_1<VAR>Ring R<VAR>x y : R<GOAL>CompleteOrthogonalIdempotents ![x, y] ↔ IsIdempotentElem x ∧ y = 1 - x
<VAR>R : Type u_1<VAR>Ring R<VAR>e : R<VAR>he : IsIdempotentElem e<GOAL>CompleteOrthogonalIdempotents ![e, 1 - e]
<VAR>I : Type u_4<VAR>Fintype I<VAR>DecidableEq I<VAR>R : I → Type u_5<VAR>(i : I) → Ring (R i)<GOAL>CompleteOrthogonalIdempotents fun x => Pi.single x 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>Fintype I<VAR>he : CompleteOrthogonalIdempotents e<GOAL>CompleteOrthogonalIdempotents (⇑f ∘ e)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>Fintype I<VAR>hf : Function.Injective ⇑f<GOAL>CompleteOrthogonalIdempotents (⇑f ∘ e) ↔ CompleteOrthogonalIdempotents e
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>Fintype I<VAR>J : Type u_4<VAR>Fintype J<VAR>i : J ≃ I<GOAL>CompleteOrthogonalIdempotents (e ∘ ⇑i) ↔ CompleteOrthogonalIdempotents e
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>Fintype I<VAR>he : OrthogonalIdempotents e<GOAL>CompleteOrthogonalIdempotents fun x => x.elim (1 - ∑ i : I, e i) e
<VAR>R : Type u_1<VAR>Ring R<VAR>I : Type u_3<VAR>e : I → R<VAR>Fintype I<VAR>Subsingleton R<GOAL>CompleteOrthogonalIdempotents e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>n : ℕ<VAR>e : Fin n → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin n), e i ∈ f.range<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>Fintype I<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : I → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : I), e i ∈ f.range<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>Ring R<VAR>e₁ e₂ : R<VAR>he₁ : IsIdempotentElem e₁<VAR>he₂ : IsIdempotentElem e₂<VAR>H : IsNilpotent (e₁ - e₂)<VAR>H' : Commute e₁ e₂<GOAL>e₁ = e₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Ring R<VAR>Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>Fintype I<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>he : ∀ (i : I), IsIdempotentElem (e i)<VAR>he' : ∀ (i : I), IsMulCentral (e i)<VAR>he'' : CompleteOrthogonalIdempotents (⇑f ∘ e)<GOAL>CompleteOrthogonalIdempotents e
<VAR>R : Type u_1<VAR>CommRing R<VAR>e₁ e₂ : R<VAR>he₁ : IsIdempotentElem e₁<VAR>he₂ : IsIdempotentElem e₂<VAR>H : IsNilpotent (e₁ - e₂)<GOAL>e₁ = e₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>f : R →+* S<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>e : S<VAR>he : e ∈ f.range<VAR>he' : IsIdempotentElem e<GOAL>∃! e', IsIdempotentElem e' ∧ f e' = e
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Type u_3<VAR>Finite I<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<GOAL>Function.Surjective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>he : ∀ (i : I), IsIdempotentElem (e i)<VAR>he' : CompleteOrthogonalIdempotents (⇑f ∘ e)<GOAL>CompleteOrthogonalIdempotents e
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<GOAL>∏ i : I, (1 - e i) = 1 - ∑ i : I, e i
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<VAR>he : CompleteOrthogonalIdempotents e<GOAL>∏ i : I, (1 - e i) = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<VAR>he : OrthogonalIdempotents e<VAR>he' : ∏ i : I, (1 - e i) = 0<GOAL>CompleteOrthogonalIdempotents e
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<VAR>he : CompleteOrthogonalIdempotents e<GOAL>Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {1 - e i}))
<VAR>R : Type u_1<VAR>CommRing R<VAR>I : Type u_3<VAR>Fintype I<VAR>e : I → R<VAR>he : CompleteOrthogonalIdempotents fun x => 1 - e x<GOAL>Function.Bijective ⇑(Pi.ringHom fun i => Ideal.Quotient.mk (Ideal.span {e i}))