ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>r : R<VAR>hr : IsUnit r<VAR>H : Function.Bijective ⇑(algebraMap R S)<GOAL>IsLocalization.Away r S
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommRing R<VAR>CommRing S<VAR>Algebra R S<VAR>e : R<VAR>he : IsIdempotentElem e<VAR>H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}<VAR>H' : Function.Surjective ⇑(algebraMap R S)<GOAL>IsLocalization.Away e S
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>n : ℤ<VAR>hn : 0 ≤ n<GOAL>selfZPow x B n = (algebraMap R B) x ^ n.natAbs
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>d : ℕ<GOAL>selfZPow x B ↑d = (algebraMap R B) x ^ d
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<GOAL>selfZPow x B 0 = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>n : ℤ<VAR>hn : n < 0<GOAL>selfZPow x B n = IsLocalization.mk' B 1 (Submonoid.pow x n.natAbs)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>n : ℤ<VAR>hn : n ≤ 0<GOAL>selfZPow x B n = IsLocalization.mk' B 1 (Submonoid.pow x n.natAbs)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>d : ℕ<GOAL>selfZPow x B (-↑d) = IsLocalization.mk' B 1 (Submonoid.pow x d)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>n m : ℕ<GOAL>selfZPow x B (↑n - ↑m) = IsLocalization.mk' B (x ^ n) (Submonoid.pow x m)
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>n m : ℤ<GOAL>selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>d : ℤ<GOAL>selfZPow x B d * selfZPow x B (-d) = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>d : ℤ<GOAL>selfZPow x B (-d) * selfZPow x B d = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>a : R<VAR>b : B<VAR>m d : ℤ<GOAL>selfZPow x B (m - d) * IsLocalization.mk' B a 1 = b ↔ selfZPow x B m * IsLocalization.mk' B a 1 = selfZPow x B d * b
<VAR>R : Type u_1<VAR>CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>CommRing B<VAR>Algebra R B<VAR>IsLocalization.Away x B<VAR>IsDomain R<VAR>WfDvdMonoid R<VAR>b : B<VAR>hb : b ≠ 0<VAR>hx : Irreducible x<GOAL>∃ a n, ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b
<VAR>R : Type u_1<VAR>Semiring R<VAR>self : LocalRing R<VAR>a b : R<VAR>h : a + b = 1<GOAL>IsUnit a ∨ IsUnit b
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>p : Associates M<VAR>h₁ : p ≠ 0<GOAL>IsAtom p ↔ Irreducible p
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>p : Associates M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hp : Prime p<GOAL>∃ c, c 1 = p ∧ StrictMono c ∧ ∀ {r : Associates M}, r ≤ p ^ n ↔ ∃ i, r = c i
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>i_pos : i ≠ 0<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<GOAL>¬IsUnit (c i)
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>n : ℕ<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<GOAL>IsUnit (c 0)
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>hq : q ≠ 0<GOAL>Irreducible (c 1)
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>p q r : Associates M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>hp : Prime p<VAR>hr : r ∣ q<VAR>hp' : p ∣ r<GOAL>p = c 1
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>q : Associates M<VAR>n : ℕ<VAR>c : Fin (n + 1) → Associates M<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>m : Finset (Associates M)<VAR>hm : ∀ r ∈ m, r ≤ q<GOAL>m.card ≤ n + 1
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>UniqueFactorizationMonoid M<VAR>q r : Associates M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>hr : r ∣ q<VAR>hq : q ≠ 0<GOAL>∃ i, r = c 1 ^ ↑i
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>UniqueFactorizationMonoid M<VAR>q : Associates M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>hq : q ≠ 0<GOAL>q = c 1 ^ n
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>UniqueFactorizationMonoid M<VAR>q : Associates M<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>c : Fin (n + 1) → Associates M<VAR>h₁ : StrictMono c<VAR>h₂ : ∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i<VAR>hq : q ≠ 0<GOAL>IsPrimePow q
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>m : Associates M<VAR>n : Associates N<VAR>d : { l // l ≤ m } ≃o { l // l ≤ n }<GOAL>↑(d ⟨1, ⋯⟩) = 1
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>m u : Associates M<VAR>n : Associates N<VAR>hu' : u ≤ m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>↑(d ⟨u, hu'⟩) = 1 ↔ u = 1
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>UniqueFactorizationMonoid N<VAR>UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<VAR>s : ℕ<VAR>hs' : p ^ s ≤ m<GOAL>↑(d ⟨p, ⋯⟩) ^ s ≤ n
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>UniqueFactorizationMonoid N<VAR>UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>Prime ↑(d ⟨p, ⋯⟩)
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>UniqueFactorizationMonoid N<VAR>UniqueFactorizationMonoid M<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>↑(d ⟨p, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors n
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>UniqueFactorizationMonoid N<VAR>UniqueFactorizationMonoid M<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>m p : Associates M<VAR>n : Associates N<VAR>hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>multiplicity p m ≤ multiplicity (↑(d ⟨p, ⋯⟩)) n
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>UniqueFactorizationMonoid N<VAR>UniqueFactorizationMonoid M<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>m p : Associates M<VAR>n : Associates N<VAR>hn : n ≠ 0<VAR>hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m<VAR>d : ↑(Set.Iic m) ≃o ↑(Set.Iic n)<GOAL>multiplicity p m = multiplicity (↑(d ⟨p, ⋯⟩)) n
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>Unique Mˣ<VAR>Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>l : ↑(Set.Iic (Associates.mk n))<GOAL>↑((RelIso.symm (mkFactorOrderIsoOfFactorDvdEquiv hd)) l) = Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩)
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>Unique Mˣ<VAR>Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>l : ↑(Set.Iic (Associates.mk m))<GOAL>↑((mkFactorOrderIsoOfFactorDvdEquiv hd) l) = Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩)
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>Unique Mˣ<VAR>Unique Nˣ<VAR>UniqueFactorizationMonoid M<VAR>UniqueFactorizationMonoid N<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<GOAL>↑(d ⟨p, ⋯⟩) ∈ UniqueFactorizationMonoid.normalizedFactors n
<VAR>M : Type u_1<VAR>CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>CancelCommMonoidWithZero N<VAR>Unique Mˣ<VAR>Unique Nˣ<VAR>UniqueFactorizationMonoid M<VAR>UniqueFactorizationMonoid N<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>DecidableRel fun x x_1 => x ∣ x_1<VAR>m p : M<VAR>n : N<VAR>hm : m ≠ 0<VAR>hn : n ≠ 0<VAR>hp : p ∈ UniqueFactorizationMonoid.normalizedFactors m<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<GOAL>multiplicity (↑(d ⟨p, ⋯⟩)) n = multiplicity p m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>self : IsLocalRingHom f<VAR>a : R<GOAL>IsUnit (f a) → IsUnit a
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>P : Ideal R<VAR>hp : P.IsPrime<VAR>NoZeroDivisors R<GOAL>P.primeCompl ≤ nonZeroDivisors R
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>P : Ideal R<VAR>hp : P.IsPrime<VAR>IsLocalization.AtPrime S P<GOAL>Nontrivial S
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>P : Ideal R<VAR>hp : P.IsPrime<VAR>IsLocalization.AtPrime S P<GOAL>LocalRing S
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>IsLocalization.AtPrime S I<VAR>x : R<GOAL>IsUnit ((algebraMap R S) x) ↔ x ∈ I.primeCompl
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>IsLocalization.AtPrime S I<VAR>x : R<VAR>h : LocalRing S := ⋯<GOAL>(algebraMap R S) x ∈ LocalRing.maximalIdeal S ↔ x ∈ I
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>IsLocalization.AtPrime S I<VAR>h : LocalRing S := ⋯<GOAL>Ideal.comap (algebraMap R S) (LocalRing.maximalIdeal S) = I
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>IsLocalization.AtPrime S I<VAR>x : R<VAR>y : ↥I.primeCompl<GOAL>IsUnit (IsLocalization.mk' S x y) ↔ x ∈ I.primeCompl
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Type u_2<VAR>CommSemiring S<VAR>Algebra R S<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>IsLocalization.AtPrime S I<VAR>x : R<VAR>y : ↥I.primeCompl<VAR>h : LocalRing S := ⋯<GOAL>IsLocalization.mk' S x y ∈ LocalRing.maximalIdeal S ↔ x ∈ I
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<GOAL>Ideal.comap (algebraMap R (Localization.AtPrime I)) (LocalRing.maximalIdeal (Localization I.primeCompl)) = I
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<GOAL>Ideal.map (algebraMap R (Localization.AtPrime I)) I = LocalRing.maximalIdeal (Localization I.primeCompl)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>P : Type u_3<VAR>CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>J : Ideal P<VAR>hJ : J.IsPrime<VAR>f : R →+* P<GOAL>I.primeCompl ≤ Submonoid.comap f J.primeCompl ↔ Ideal.comap f J ≤ I
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>P : Type u_3<VAR>CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>J : Ideal P<VAR>J.IsPrime<VAR>f : R →+* P<VAR>hIJ : I = Ideal.comap f J<VAR>x : R<GOAL>(Localization.localRingHom I J f hIJ) ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>P : Type u_3<VAR>CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>J : Ideal P<VAR>J.IsPrime<VAR>f : R →+* P<VAR>hIJ : I = Ideal.comap f J<VAR>x : R<VAR>y : ↥I.primeCompl<GOAL>(Localization.localRingHom I J f hIJ) (IsLocalization.mk' (Localization.AtPrime I) x y) = IsLocalization.mk' (Localization.AtPrime J) (f x) ⟨f ↑y, ⋯⟩
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>P : Type u_3<VAR>CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>J : Ideal P<VAR>J.IsPrime<VAR>f : R →+* P<VAR>hIJ : I = Ideal.comap f J<VAR>j : Localization.AtPrime I →+* Localization.AtPrime J<VAR>hj : ∀ (x : R), j ((algebraMap R (Localization.AtPrime I)) x) = (algebraMap P (Localization.AtPrime J)) (f x)<GOAL>Localization.localRingHom I J f hIJ = j
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>I : Ideal R<VAR>hI : I.IsPrime<GOAL>Localization.localRingHom I I (RingHom.id R) ⋯ = RingHom.id (Localization.AtPrime I)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>P : Type u_3<VAR>CommSemiring P<VAR>I : Ideal R<VAR>hI : I.IsPrime<VAR>S : Type u_4<VAR>CommSemiring S<VAR>J : Ideal S<VAR>hJ : J.IsPrime<VAR>K : Ideal P<VAR>hK : K.IsPrime<VAR>f : R →+* S<VAR>hIJ : I = Ideal.comap f J<VAR>g : S →+* P<VAR>hJK : J = Ideal.comap g K<GOAL>Localization.localRingHom I K (g.comp f) ⋯ = (Localization.localRingHom J K g hJK).comp (Localization.localRingHom I J f hIJ)
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>IsLocalization S A<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_4<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>Module A M'<VAR>IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>IsLocalizedModule S f<GOAL>IsBaseChange A f
<VAR>R : Type u_1<VAR>CommSemiring R<VAR>S : Submonoid R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>IsLocalization S A<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>Module R M<VAR>M' : Type u_4<VAR>AddCommMonoid M'<VAR>Module R M'<VAR>Module A M'<VAR>IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<GOAL>IsLocalizedModule S f ↔ IsBaseChange A f
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : R<GOAL>(algebraMap R K) x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>Function.Injective ⇑(algebraMap R K)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>a b : R<GOAL>↑a = ↑b ↔ a = b
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>Nontrivial R<VAR>x : R<VAR>hx : x ∈ nonZeroDivisors R<GOAL>(algebraMap R K) x ≠ 0
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra A K<VAR>IsFractionRing A K<GOAL>IsDomain K
<VAR>A : Type u_6<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_7<VAR>CommRing K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>z : K<GOAL>IsFractionRing.inv A z = if h : z = 0 then 0 else IsLocalization.mk' K ↑(IsLocalization.sec (nonZeroDivisors A) z).2 ⟨(IsLocalization.sec (nonZeroDivisors A) z).1, ⋯⟩
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>x * IsFractionRing.inv A x = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>IsDomain R<GOAL>Function.Surjective ⇑(algebraMap R K) ↔ IsField R
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>r s : A<VAR>hs : s ∈ nonZeroDivisors A<GOAL>IsLocalization.mk' K r ⟨s, hs⟩ = (algebraMap A K) r / (algebraMap A K) s
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>r : A<VAR>s : ↥(nonZeroDivisors A)<GOAL>IsLocalization.mk' K r s = (algebraMap A K) r / (algebraMap A K) ↑s
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>z : K<GOAL>∃ x, ∃ y ∈ nonZeroDivisors A, (algebraMap A K) x / (algebraMap A K) y = z
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>L : Type u_7<VAR>Field L<VAR>g : A →+* L<VAR>hg : Function.Injective ⇑g<VAR>y : ↥(nonZeroDivisors A)<GOAL>IsUnit (g ↑y)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>Field K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>x : R<VAR>y : ↥(nonZeroDivisors R)<GOAL>IsLocalization.mk' K x y = 0 ↔ x = 0
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_5<VAR>Field K<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>x : A<VAR>y : ↥(nonZeroDivisors A)<GOAL>IsLocalization.mk' K x y = 1 ↔ x = ↑y
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_5<VAR>Field K<VAR>L : Type u_7<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>g : A →+* L<VAR>hg : Function.Injective ⇑g<VAR>x : A<GOAL>(IsFractionRing.lift hg) ((algebraMap A K) x) = g x
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>K : Type u_5<VAR>Field K<VAR>L : Type u_7<VAR>Field L<VAR>Algebra A K<VAR>IsFractionRing A K<VAR>g : A →+* L<VAR>hg : Function.Injective ⇑g<VAR>x : A<VAR>y : ↥(nonZeroDivisors A)<GOAL>(IsFractionRing.lift hg) (IsLocalization.mk' K x y) = g x / g ↑y
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>P : Type u_3<VAR>CommRing P<VAR>h : R ≃+* P<GOAL>IsFractionRing R S ↔ IsFractionRing P S
<VAR>R : Type u_8<VAR>S : Type u_9<VAR>CommRing R<VAR>Nontrivial R<VAR>CommRing S<VAR>Algebra R S<VAR>IsFractionRing R S<GOAL>Nontrivial S
<VAR>A : Type u_4<VAR>CommRing A<VAR>IsDomain A<VAR>r : A<VAR>s : ↥(nonZeroDivisors A)<GOAL>Localization.mk r s = (algebraMap A (FractionRing A)) r / (algebraMap A (FractionRing A)) ↑s
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I : Ideal R<VAR>x : S<GOAL>x ∈ IsLocalization.coeSubmodule S I ↔ ∃ y ∈ I, (algebraMap R S) y = x
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I J : Ideal R<VAR>h : I ≤ J<GOAL>IsLocalization.coeSubmodule S I ≤ IsLocalization.coeSubmodule S J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<GOAL>IsLocalization.coeSubmodule S ⊥ = ⊥
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<GOAL>IsLocalization.coeSubmodule S ⊤ = 1
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I J : Ideal R<GOAL>IsLocalization.coeSubmodule S (I ⊔ J) = IsLocalization.coeSubmodule S I ⊔ IsLocalization.coeSubmodule S J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>I J : Ideal R<GOAL>IsLocalization.coeSubmodule S (I * J) = IsLocalization.coeSubmodule S I * IsLocalization.coeSubmodule S J
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>hS : Function.Injective ⇑(algebraMap R S)<VAR>I : Ideal R<GOAL>(IsLocalization.coeSubmodule S I).FG ↔ Submodule.FG I
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>s : Set R<GOAL>IsLocalization.coeSubmodule S (Ideal.span s) = Submodule.span R (⇑(algebraMap R S) '' s)
<VAR>R : Type u_1<VAR>CommRing R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>x : R<GOAL>IsLocalization.coeSubmodule S (Ideal.span {x}) = Submodule.span R {(algebraMap R S) x}
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>h : IsNoetherianRing R<GOAL>IsNoetherianRing S
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>h : M ≤ nonZeroDivisors R<VAR>I J : Ideal R<GOAL>IsLocalization.coeSubmodule S I ≤ IsLocalization.coeSubmodule S J ↔ I ≤ J
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>h : M ≤ nonZeroDivisors R<GOAL>StrictMono (IsLocalization.coeSubmodule S)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>h : M ≤ nonZeroDivisors R<GOAL>Function.Injective (IsLocalization.coeSubmodule S)
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>I : Ideal R<VAR>h : M ≤ nonZeroDivisors R<GOAL>(IsLocalization.coeSubmodule S I).IsPrincipal ↔ Submodule.IsPrincipal I
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>N : Type u_5<VAR>AddCommGroup N<VAR>Module R N<VAR>Module S N<VAR>IsScalarTower R S N<VAR>x : N<VAR>a : Set N<GOAL>x ∈ Submodule.span S a ↔ ∃ y ∈ Submodule.span R a, ∃ z, x = IsLocalization.mk' S 1 z • y
<VAR>R : Type u_1<VAR>CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>IsLocalization M S<VAR>x : S<VAR>a : Set R<GOAL>x ∈ Ideal.span (⇑(algebraMap R S) '' a) ↔ ∃ y ∈ Ideal.span a, ∃ z, x = IsLocalization.mk' S y z
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I J : Ideal R<GOAL>IsLocalization.coeSubmodule K I ≤ IsLocalization.coeSubmodule K J ↔ I ≤ J
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>StrictMono (IsLocalization.coeSubmodule K)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<GOAL>Function.Injective (IsLocalization.coeSubmodule K)
<VAR>R : Type u_1<VAR>CommRing R<VAR>K : Type u_5<VAR>CommRing K<VAR>Algebra R K<VAR>IsFractionRing R K<VAR>I : Ideal R<GOAL>(IsLocalization.coeSubmodule K I).IsPrincipal ↔ Submodule.IsPrincipal I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>IsLocalRingHom f<VAR>a : R<GOAL>IsUnit (f a) ↔ IsUnit a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>IsLocalRingHom f<VAR>a : R<GOAL>f a ∈ nonunits S ↔ a ∈ nonunits R
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>IsLocalRingHom f<VAR>a : R<VAR>h : IsUnit (f a)<GOAL>IsUnit a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Semiring R<VAR>Semiring S<VAR>f : R →+* S<VAR>h : IsLocalRingHom f<VAR>x : R<VAR>hfx : Irreducible (f x)<GOAL>Irreducible x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>Semiring R<VAR>Semiring S<VAR>Semiring T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>IsLocalRingHom (g.comp f)<GOAL>IsLocalRingHom f
<VAR>R : Type u_4<VAR>S : Type u_5<VAR>CommSemiring R<VAR>CommSemiring S<VAR>H : LocalRing S<VAR>f : R →+* S<VAR>IsLocalRingHom f<GOAL>LocalRing R
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>LocalRing R<VAR>CommSemiring S<VAR>LocalRing S<VAR>f : R →+* S<VAR>IsLocalRingHom f<VAR>a : R<VAR>h : a ∈ LocalRing.maximalIdeal R<GOAL>f a ∈ LocalRing.maximalIdeal S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>LocalRing R<VAR>CommSemiring S<VAR>LocalRing S<VAR>f : R →+* S<GOAL>[IsLocalRingHom f, ⇑f '' ↑(LocalRing.maximalIdeal R).toAddSubmonoid ⊆ ↑(LocalRing.maximalIdeal S), Ideal.map f (LocalRing.maximalIdeal R) ≤ LocalRing.maximalIdeal S, LocalRing.maximalIdeal R ≤ Ideal.comap f (LocalRing.maximalIdeal S), Ideal.comap f (LocalRing.maximalIdeal S) = LocalRing.maximalIdeal R].TFAE
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommSemiring R<VAR>LocalRing R<VAR>CommSemiring S<VAR>Nontrivial S<VAR>f : R →+* S<VAR>IsLocalRingHom f<VAR>hf : Function.Surjective ⇑f<GOAL>LocalRing S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>h : IsLocalRingHom f<GOAL>Function.Surjective ⇑(Units.map ↑f)
<VAR>A : Type u_4<VAR>B : Type u_5<VAR>CommSemiring A<VAR>LocalRing A<VAR>CommSemiring B<VAR>e : A ≃+* B<GOAL>LocalRing B
<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>self : HomogeneousLocalization.NumDenSameDeg 𝒜 x<GOAL>↑self.den ∈ x