# Localizations away from an element #

## Main definitions #

- `IsLocalization.Away (x : R) S` expresses that `S` is a localization away from `x`, as an abbreviation of `IsLocalization (Submonoid.powers x) S`.
- `exists_reduced_fraction' (hb : b ≠ 0)` produces a reduced fraction of the form `b = a * x^n` for some `n : ℤ` and some `a : R` that is not divisible by `x`.

## Implementation notes #

See `Mathlib/RingTheory/Localization/Basic.lean` for a design overview.

## Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

source
@[reducible, inline]
abbrev IsLocalization.Away {R : Type u_1} [CommSemiring R] (x : R) (S : Type u_4) [CommSemiring S] [Algebra R S] :
Prop

Given `x : R`, the typeclass `IsLocalization.Away x S` states that `S` is isomorphic to the localization of `R` at the submonoid generated by `x`. See `IsLocalization.Away.mk` for a specialized constructor.

Equations

- IsLocalization.Away x S = IsLocalization (Submonoid.powers x) S

Instances For

source
noncomputable def IsLocalization.Away.invSelf {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] :
S

Given `x : R` and a localization map `F : R →+* S` away from `x`, `invSelf` is `(F x)⁻¹`.

Equations

- IsLocalization.Away.invSelf x = IsLocalization.mk' S 1 ⟨x, ⋯⟩

Instances For

source
@[simp]
theorem IsLocalization.Away.mul_invSelf {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] :
(algebraMap R S) x * invSelf x = 1
source
noncomputable def IsLocalization.Away.sec {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] (s : S) :
R × ℕ

For `s : S` with `S` being the localization of `R` away from `x`, this is a choice of `(r, n) : R × ℕ` such that `s * algebraMap R S (x ^ n) = algebraMap R S r`.

Equations

- IsLocalization.Away.sec x s = ((IsLocalization.sec (Submonoid.powers x) s).1, Exists.choose ⋯)

Instances For

source
theorem IsLocalization.Away.sec_spec {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] (s : S) :
s * (algebraMap R S) (x ^ (sec x s).2) = (algebraMap R S) (sec x s).1
source
theorem IsLocalization.Away.algebraMap_pow_isUnit {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] (n : ℕ) :
IsUnit ((algebraMap R S) x ^ n)
source
theorem IsLocalization.Away.algebraMap_isUnit {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] :
IsUnit ((algebraMap R S) x)
source
theorem IsLocalization.Away.associated_sec_fst {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] (s : S) :
Associated ((algebraMap R S) (sec x s).1) s
source
theorem IsLocalization.Away.algebraMap_isUnit_iff {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] {y : R} :
IsUnit ((algebraMap R S) y) ↔ ∃ (n : ℕ), y ∣ x ^ n
source
theorem IsLocalization.Away.surj {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] (z : S) :
∃ (n : ℕ) (a : R), z * (algebraMap R S) x ^ n = (algebraMap R S) a
source
theorem IsLocalization.Away.exists_of_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] {a b : R} (h : (algebraMap R S) a = (algebraMap R S) b) :
∃ (n : ℕ), x ^ n * a = x ^ n * b
source
theorem IsLocalization.Away.mk {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (r : R) (map_unit : IsUnit ((algebraMap R S) r)) (surj : ∀ (s : S), ∃ (n : ℕ) (a : R), s * (algebraMap R S) r ^ n = (algebraMap R S) a) (exists_of_eq : ∀ (a b : R), (algebraMap R S) a = (algebraMap R S) b → ∃ (n : ℕ), r ^ n * a = r ^ n * b) :
Away r S

Specialized constructor for `IsLocalization.Away`.

source
theorem IsLocalization.Away.of_associated {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {r r' : R} (h : Associated r r') [Away r S] :
Away r' S
source
theorem IsLocalization.Away.iff_of_associated {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {r r' : R} (h : Associated r r') :
Away r S ↔ Away r' S

If `r` and `r'` are associated elements of `R`, an `R`-algebra `S` is the localization of `R` away from `r` if and only if it is the localization of `R` away from `r'`.

source
theorem IsLocalization.Away.isUnit_of_dvd {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (x : R) [Away x S] {r : R} (h : r ∣ x) :
IsUnit ((algebraMap R S) r)
source
noncomputable def IsLocalization.Away.lift {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [Away x S] {g : R →+* P} (hg : IsUnit (g x)) :
S →+* P

Given `x : R`, a localization map `F : R →+* S` away from `x`, and a map of `CommSemiring`s `g : R →+* P` such that `g x` is invertible, the homomorphism induced from `S` to `P` sending `z : S` to `g y * (g x)⁻ⁿ`, where `y : R, n : ℕ` are such that `z = F y * (F x)⁻ⁿ`.

Equations

- IsLocalization.Away.lift x hg = IsLocalization.lift ⋯

Instances For

source
@[simp]
theorem IsLocalization.Away.lift_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [Away x S] {g : R →+* P} (hg : IsUnit (g x)) (a : R) :
(lift x hg) ((algebraMap R S) a) = g a
source
@[simp]
theorem IsLocalization.Away.lift_comp {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [Away x S] {g : R →+* P} (hg : IsUnit (g x)) :
(lift x hg).comp (algebraMap R S) = g
source
noncomputable def IsLocalization.Away.awayToAwayLeft {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [Away x S] (y : R) [Algebra R P] [Away (y * x) P] :
S →+* P

Given `x y : R` and localizations `S`, `P` away from `x` and `y * x` respectively, the homomorphism induced from `S` to `P`.

Equations

- IsLocalization.Away.awayToAwayLeft x y = IsLocalization.Away.lift x ⋯

Instances For

source
noncomputable def IsLocalization.Away.awayToAwayRight {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [Away x S] (y : R) [Algebra R P] [Away (x * y) P] :
S →+* P

Given `x y : R` and localizations `S`, `P` away from `x` and `x * y` respectively, the homomorphism induced from `S` to `P`.

Equations

- IsLocalization.Away.awayToAwayRight x y = IsLocalization.Away.lift x ⋯

Instances For

source
theorem IsLocalization.Away.awayToAwayLeft_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [Away x S] (y : R) [Algebra R P] [Away (y * x) P] (a : R) :
(awayToAwayLeft x y) ((algebraMap R S) a) = (algebraMap R P) a
source
theorem IsLocalization.Away.awayToAwayRight_eq {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (x : R) [Away x S] (y : R) [Algebra R P] [Away (x * y) P] (a : R) :
(awayToAwayRight x y) ((algebraMap R S) a) = (algebraMap R P) a
source
noncomputable def IsLocalization.Away.map {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] {P : Type u_3} [CommSemiring P] (Q : Type u_4) [CommSemiring Q] [Algebra P Q] (f : R →+* P) (r : R) [Away r S] [Away (f r) Q] :
S →+* Q

Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`.

Equations

- IsLocalization.Away.map S Q f r = IsLocalization.map Q f ⋯

Instances For

source
instance IsLocalization.Away.instMapRingHomPowersOfCoe {A : Type u_5} [CommSemiring A] {B : Type u_6} [CommSemiring B] (Bₚ : Type u_8) [CommSemiring Bₚ] [Algebra B Bₚ] {f : A →+* B} (a : A) [Away (f a) Bₚ] :
IsLocalization (Submonoid.map f (Submonoid.powers a)) Bₚ
source
instance IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] (Aₚ : Type u_7) [CommSemiring Aₚ] [Algebra A Aₚ] (x : R) [Away ((algebraMap R A) x) Aₚ] :
IsLocalization (Algebra.algebraMapSubmonoid A (Submonoid.powers x)) Aₚ
source
noncomputable def IsLocalization.Away.mapₐ {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] (Aₚ : Type u_7) [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] (Bₚ : Type u_8) [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] (f : A →ₐ[R] B) (a : A) [Away a Aₚ] [Away (f a) Bₚ] :
Aₚ →ₐ[R] Bₚ

Given a algebra map `f : A →ₐ[R] B` and an element `a : A`, we may construct a map `Aₐ →ₐ[R] Bₐ`.

Equations

- IsLocalization.Away.mapₐ Aₚ Bₚ f a = { toRingHom := IsLocalization.Away.map Aₚ Bₚ f.toRingHom a, commutes' := ⋯ }

Instances For

source
@[simp]
theorem IsLocalization.Away.mapₐ_apply {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] (Aₚ : Type u_7) [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] (Bₚ : Type u_8) [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] (f : A →ₐ[R] B) (a : A) [Away a Aₚ] [Away (f a) Bₚ] (x : Aₚ) :
(mapₐ Aₚ Bₚ f a) x = (map Aₚ Bₚ f.toRingHom a) x
source
theorem IsLocalization.Away.mapₐ_injective_of_injective {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] {Aₚ : Type u_7} [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] {Bₚ : Type u_8} [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ] (hf : Function.Injective ⇑f) :
Function.Injective ⇑(mapₐ Aₚ Bₚ f a)
source
theorem IsLocalization.Away.mapₐ_surjective_of_surjective {R : Type u_1} [CommSemiring R] {A : Type u_5} [CommSemiring A] [Algebra R A] {B : Type u_6} [CommSemiring B] [Algebra R B] {Aₚ : Type u_7} [CommSemiring Aₚ] [Algebra A Aₚ] [Algebra R Aₚ] [IsScalarTower R A Aₚ] {Bₚ : Type u_8} [CommSemiring Bₚ] [Algebra B Bₚ] [Algebra R Bₚ] [IsScalarTower R B Bₚ] {f : A →ₐ[R] B} (a : A) [Away a Aₚ] [Away (f a) Bₚ] (hf : Function.Surjective ⇑f) :
Function.Surjective ⇑(mapₐ Aₚ Bₚ f a)
source
theorem IsLocalization.Away.mul {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_5) [CommSemiring T] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (x y : R) [Away x S] [Away ((algebraMap R S) y) T] :
Away (y * x) T

Localizing the localization of `R` at `x` at the image of `y` is the same as localizing `R` at `y * x`. See `IsLocalization.Away.mul'` for the `x * y` version.

source
theorem IsLocalization.Away.mul' {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (T : Type u_5) [CommSemiring T] [Algebra S T] [Algebra R T] [IsScalarTower R S T] (x y : R) [Away x S] [Away ((algebraMap R S) y) T] :
Away (x * y) T

Localizing the localization of `R` at `x` at the image of `y` is the same as localizing `R` at `x * y`. See `IsLocalization.Away.mul` for the `y * x` version.

source
instance IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (x y : R) [Away x S] :
Away (y * x) (Localization.Away ((algebraMap R S) y))

Localizing the localization of `R` at `x` at the image of `y` is the same as localizing `R` at `y * x`.

source
instance IsLocalization.Away.instHMulAwayCoeRingHomAlgebraMap_1 {R : Type u_1} [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (x y : R) [Away x S] :
Away (x * y) (Localization.Away ((algebraMap R S) y))

Localizing the localization of `R` at `x` at the image of `y` is the same as localizing `R` at `x * y`.

source
theorem IsLocalization.Away.commutes {R : Type u_5} [CommSemiring R] (S₁ : Type u_6) (S₂ : Type u_7) (T : Type u_8) [CommSemiring S₁] [CommSemiring S₂] [CommSemiring T] [Algebra R S₁] [Algebra R S₂] [Algebra R T] [Algebra S₁ T] [Algebra S₂ T] [IsScalarTower R S₁ T] [IsScalarTower R S₂ T] (x y : R) [Away x S₁] [Away y S₂] [Away ((algebraMap R S₂) x) T] :
Away ((algebraMap R S₁) y) T

If `S₁` is the localization of `R` away from `f` and `S₂` is the localization away from `g`, then any localization `T` of `S₂` away from `f` is also a localization of `S₁` away from `g`.

source
noncomputable def IsLocalization.atUnit (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] (x : R) (e : IsUnit x) [Away x S] :
R ≃ₐ[R] S

The localization away from a unit is isomorphic to the ring.

Equations

- IsLocalization.atUnit R S x e = IsLocalization.atUnits R (Submonoid.powers x) ⋯

Instances For

source
noncomputable def IsLocalization.atOne (R : Type u_1) [CommSemiring R] (S : Type u_2) [CommSemiring S] [Algebra R S] [Away 1 S] :
R ≃ₐ[R] S

The localization at one is isomorphic to the ring.

Equations

- IsLocalization.atOne R S = IsLocalization.atUnit R S 1 ⋯

Instances For

source
theorem IsLocalization.away_of_isUnit_of_bijective {R : Type u_4} (S : Type u_5) [CommSemiring R] [CommSemiring S] [Algebra R S] {r : R} (hr : IsUnit r) (H : Function.Bijective ⇑(algebraMap R S)) :
Away r S
source
theorem IsLocalization.away_of_isIdempotentElem_of_mul {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [Algebra R S] {e : R} (he : IsIdempotentElem e) (H : ∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y) (H' : Function.Surjective ⇑(algebraMap R S)) :
Away e S
source
theorem IsLocalization.away_of_isIdempotentElem {R : Type u_4} {S : Type u_5} [CommRing R] [CommRing S] [Algebra R S] {e : R} (he : IsIdempotentElem e) (H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}) (H' : Function.Surjective ⇑(algebraMap R S)) :
Away e S
source
instance IsLocalization.away_fst {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] :
Away (1, 0) R
source
instance IsLocalization.away_snd {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] :
Away (0, 1) S
source
@[reducible, inline]
noncomputable abbrev Localization.awayLift {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (f : R →+* P) (r : R) (hr : IsUnit (f r)) :
Away r →+* P

Given a map `f : R →+* S` and an element `r : R`, such that `f r` is invertible, we may construct a map `Rᵣ →+* S`.

Equations

- Localization.awayLift f r hr = IsLocalization.Away.lift r hr

Instances For

source
theorem Localization.awayLift_mk {R : Type u_1} [CommSemiring R] {A : Type u_4} [CommSemiring A] (f : R →+* A) (r a : R) (v : A) (hv : f r * v = 1) (j : ℕ) :
(awayLift f r ⋯) (mk a ⟨r ^ j, ⋯⟩) = f a * v ^ j
source
@[reducible, inline]
noncomputable abbrev Localization.awayMap {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (f : R →+* P) (r : R) :
Away r →+* Away (f r)

Given a map `f : R →+* S` and an element `r : R`, we may construct a map `Rᵣ →+* Sᵣ`.

Equations

- Localization.awayMap f r = IsLocalization.Away.map (Localization.Away r) (Localization.Away (f r)) f r

Instances For

source
@[reducible, inline]
noncomputable abbrev Localization.awayMapₐ {R : Type u_1} [CommSemiring R] {A : Type u_4} [CommSemiring A] [Algebra R A] {B : Type u_5} [CommSemiring B] [Algebra R B] (f : A →ₐ[R] B) (a : A) :
Away a →ₐ[R] Away (f a)

Given a map `f : A →ₐ[R] B` and an element `a : A`, we may construct a map `Aₐ →ₐ[R] Bₐ`.

Equations

- Localization.awayMapₐ f a = IsLocalization.Away.mapₐ (Localization.Away a) (Localization.Away (f a)) f a

Instances For

source
theorem Localization.algebraMap_injective_of_span_eq_top {R : Type u_1} [CommSemiring R] (s : Set R) (span_eq : Ideal.span s = ⊤) :
Function.Injective ⇑(algebraMap R ((a : ↑s) → Away ↑a))
source
theorem Localization.existsUnique_algebraMap_eq_of_span_eq_top {R : Type u_1} [CommSemiring R] (s : Set R) (span_eq : Ideal.span s = ⊤) (f : (a : ↑s) → Away ↑a) (h : ∀ (a b : ↑s), (IsLocalization.Away.awayToAwayRight ↑a ↑b) (f a) = (IsLocalization.Away.awayToAwayLeft ↑b ↑a) (f b)) :
∃! r : R, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

The sheaf condition for the structure sheaf on `Spec R` for a covering of the whole prime spectrum by basic opens.

source
noncomputable def selfZPow {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (m : ℤ) :
B

`selfZPow x (m : ℤ)` is `x ^ m` as an element of the localization away from `x`.

Equations

- selfZPow x B m = if x_1 : 0 ≤ m then (algebraMap R B) x ^ m.natAbs else IsLocalization.mk' B 1 (Submonoid.pow x m.natAbs)

Instances For

source
theorem selfZPow_of_nonneg {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n : ℤ} (hn : 0 ≤ n) :
selfZPow x B n = (algebraMap R B) x ^ n.natAbs
source
@[simp]
theorem selfZPow_natCast {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ℕ) :
selfZPow x B ↑d = (algebraMap R B) x ^ d
source
@[simp]
theorem selfZPow_zero {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] :
selfZPow x B 0 = 1
source
theorem selfZPow_of_neg {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n : ℤ} (hn : n < 0) :
selfZPow x B n = IsLocalization.mk' B 1 (Submonoid.pow x n.natAbs)
source
theorem selfZPow_of_nonpos {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n : ℤ} (hn : n ≤ 0) :
selfZPow x B n = IsLocalization.mk' B 1 (Submonoid.pow x n.natAbs)
source
@[simp]
theorem selfZPow_neg_natCast {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ℕ) :
selfZPow x B (-↑d) = IsLocalization.mk' B 1 (Submonoid.pow x d)
source
@[simp]
theorem selfZPow_sub_natCast {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n m : ℕ} :
selfZPow x B (↑n - ↑m) = IsLocalization.mk' B (x ^ n) (Submonoid.pow x m)
source
@[simp]
theorem selfZPow_add {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] {n m : ℤ} :
selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
source
theorem selfZPow_mul_neg {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ℤ) :
selfZPow x B d * selfZPow x B (-d) = 1
source
theorem selfZPow_neg_mul {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (d : ℤ) :
selfZPow x B (-d) * selfZPow x B d = 1
source
theorem selfZPow_pow_sub {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] (a : R) (b : B) (m d : ℤ) :
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
source
theorem exists_reduced_fraction' {R : Type u_3} [CommRing R] (x : R) (B : Type u_4) [CommRing B] [Algebra R B] [IsLocalization.Away x B] [IsDomain R] [WfDvdMonoid R] {b : B} (hb : b ≠ 0) (hx : Irreducible x) :
∃ (a : R) (n : ℤ), ¬x ∣ a ∧ selfZPow x B n * (algebraMap R B) a = b