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

@[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

• Eq (IsLocalization.Away x S) (IsLocalization (Submonoid.powers x) S)

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

• Eq (IsLocalization.Away.invSelf x) (IsLocalization.mk' S 1 ⟨x, ⋯⟩)

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] : Eq (HMul.hMul (DFunLike.coe (algebraMap R S) x) (invSelf x)) 1

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) : Prod R Nat

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

• Eq (IsLocalization.Away.sec x s) { fst := (IsLocalization.sec (Submonoid.powers x) s).fst, snd := Exists.choose ⋯ }

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) : Eq (HMul.hMul s (DFunLike.coe (algebraMap R S) (HPow.hPow x (sec x s).snd))) (DFunLike.coe (algebraMap R S) (sec x s).fst)

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 : Nat) : IsUnit (HPow.hPow (DFunLike.coe (algebraMap R S) x) n)

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 (DFunLike.coe (algebraMap R S) x)

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) : Exists fun (n : Nat) => Exists fun (a : R) => Eq (HMul.hMul z (HPow.hPow (DFunLike.coe (algebraMap R S) x) n)) (DFunLike.coe (algebraMap R S) a)

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 : Eq (DFunLike.coe (algebraMap R S) a) (DFunLike.coe (algebraMap R S) b)) : Exists fun (n : Nat) => Eq (HMul.hMul (HPow.hPow x n) a) (HMul.hMul (HPow.hPow x n) b)

theorem IsLocalization.Away.mk {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommSemiring S] [Algebra R S] (r : R) (map_unit : IsUnit (DFunLike.coe (algebraMap R S) r)) (surj : ∀ (s : S), Exists fun (n : Nat) => Exists fun (a : R) => Eq (HMul.hMul s (HPow.hPow (DFunLike.coe (algebraMap R S) r) n)) (DFunLike.coe (algebraMap R S) a)) (exists_of_eq : ∀ (a b : R), Eq (DFunLike.coe (algebraMap R S) a) (DFunLike.coe (algebraMap R S) b) → Exists fun (n : Nat) => Eq (HMul.hMul (HPow.hPow r n) a) (HMul.hMul (HPow.hPow r n) b)) : Away r S

Specialized constructor for IsLocalization.Away.

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

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') : Iff (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 of it is the localization of R away from r'.

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 : Dvd.dvd r x) : IsUnit (DFunLike.coe (algebraMap R S) r)

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 : RingHom R P} (hg : IsUnit (DFunLike.coe g x)) : RingHom S P

Given x : R, a localization map F : R →+* S away from x, and a map of CommSemirings 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

• Eq (IsLocalization.Away.lift x hg) (IsLocalization.lift ⋯)

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 : RingHom R P} (hg : IsUnit (DFunLike.coe g x)) (a : R) : Eq (DFunLike.coe (lift x hg) (DFunLike.coe (algebraMap R S) a)) (DFunLike.coe g a)

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 : RingHom R P} (hg : IsUnit (DFunLike.coe g x)) : Eq ((lift x hg).comp (algebraMap R S)) g

@[deprecated IsLocalization.Away.lift_eq (since := "2024-11-25")]

theorem IsLocalization.Away.AwayMap.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 : RingHom R P} (hg : IsUnit (DFunLike.coe g x)) (a : R) : Eq (DFunLike.coe (lift x hg) (DFunLike.coe (algebraMap R S) a)) (DFunLike.coe g a)

Alias of IsLocalization.Away.lift_eq.

@[deprecated IsLocalization.Away.lift_comp (since := "2024-11-25")]

theorem IsLocalization.Away.AwayMap.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 : RingHom R P} (hg : IsUnit (DFunLike.coe g x)) : Eq ((lift x hg).comp (algebraMap R S)) g

Alias of IsLocalization.Away.lift_comp.

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 (HMul.hMul y x) P] : RingHom 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

• Eq (IsLocalization.Away.awayToAwayLeft x y) (IsLocalization.Away.lift x ⋯)

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 (HMul.hMul x y) P] : RingHom 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

• Eq (IsLocalization.Away.awayToAwayRight x y) (IsLocalization.Away.lift x ⋯)

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 (HMul.hMul y x) P] (a : R) : Eq (DFunLike.coe (awayToAwayLeft x y) (DFunLike.coe (algebraMap R S) a)) (DFunLike.coe (algebraMap R P) a)

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 (HMul.hMul x y) P] (a : R) : Eq (DFunLike.coe (awayToAwayRight x y) (DFunLike.coe (algebraMap R S) a)) (DFunLike.coe (algebraMap R P) a)

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 : RingHom R P) (r : R) [Away r S] [Away (DFunLike.coe f r) Q] : RingHom S Q

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

Equations

• Eq (IsLocalization.Away.map S Q f r) (IsLocalization.map Q f ⋯)

theorem 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 : RingHom A B} (a : A) [Away (DFunLike.coe f a) Bₚ] : IsLocalization (Submonoid.map f (Submonoid.powers a)) Bₚ

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 : AlgHom R A B) (a : A) [Away a Aₚ] [Away (DFunLike.coe f a) Bₚ] : AlgHom R Aₚ Bₚ

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

Equations

• Eq (IsLocalization.Away.mapₐ Aₚ Bₚ f a) { toRingHom := IsLocalization.Away.map Aₚ Bₚ f.toRingHom a, commutes' := ⋯ }

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 : AlgHom R A B) (a : A) [Away a Aₚ] [Away (DFunLike.coe f a) Bₚ] (x : Aₚ) : Eq (DFunLike.coe (mapₐ Aₚ Bₚ f a) x) (DFunLike.coe (map Aₚ Bₚ f.toRingHom a) x)

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 : AlgHom R A B} (a : A) [Away a Aₚ] [Away (DFunLike.coe f a) Bₚ] (hf : Function.Injective (DFunLike.coe f)) : Function.Injective (DFunLike.coe (mapₐ Aₚ Bₚ f a))

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 : AlgHom R A B} (a : A) [Away a Aₚ] [Away (DFunLike.coe f a) Bₚ] (hf : Function.Surjective (DFunLike.coe f)) : Function.Surjective (DFunLike.coe (mapₐ Aₚ Bₚ f a))

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 (DFunLike.coe (algebraMap R S) y) T] : Away (HMul.hMul 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.

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 (DFunLike.coe (algebraMap R S) y) T] : Away (HMul.hMul 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.

theorem 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 (HMul.hMul y x) (Localization.Away (DFunLike.coe (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.

theorem 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 (HMul.hMul x y) (Localization.Away (DFunLike.coe (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.

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 (DFunLike.coe (algebraMap R S₂) x) T] : Away (DFunLike.coe (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.

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] : AlgEquiv R R S

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

Equations

• Eq (IsLocalization.atUnit R S x e) (IsLocalization.atUnits R (Submonoid.powers x) ⋯)

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

The localization at one is isomorphic to the ring.

Equations

• Eq (IsLocalization.atOne R S) (IsLocalization.atUnit R S 1 ⋯)

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 (DFunLike.coe (algebraMap R S))) : Away r S

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), Iff (Eq (DFunLike.coe (algebraMap R S) x) (DFunLike.coe (algebraMap R S) y)) (Eq (HMul.hMul e x) (HMul.hMul e y))) (H' : Function.Surjective (DFunLike.coe (algebraMap R S))) : Away e S

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 : Eq (RingHom.ker (algebraMap R S)) (Ideal.span (Singleton.singleton (HSub.hSub 1 e)))) (H' : Function.Surjective (DFunLike.coe (algebraMap R S))) : Away e S

theorem IsLocalization.away_fst {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] : Away { fst := 1, snd := 0 } R

theorem IsLocalization.away_snd {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] : Away { fst := 0, snd := 1 } S

@[reducible, inline]

noncomputable abbrev Localization.awayLift {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (f : RingHom R P) (r : R) (hr : IsUnit (DFunLike.coe f r)) : RingHom (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

• Eq (Localization.awayLift f r hr) (IsLocalization.Away.lift r hr)

theorem Localization.awayLift_mk {R : Type u_1} [CommSemiring R] {A : Type u_4} [CommRing A] (f : RingHom R A) (r a : R) (v : A) (hv : Eq (HMul.hMul (DFunLike.coe f r) v) 1) (j : Nat) : Eq (DFunLike.coe (awayLift f r ⋯) (mk a ⟨HPow.hPow r j, ⋯⟩)) (HMul.hMul (DFunLike.coe f a) (HPow.hPow v j))

@[reducible, inline]

noncomputable abbrev Localization.awayMap {R : Type u_1} [CommSemiring R] {P : Type u_3} [CommSemiring P] (f : RingHom R P) (r : R) : RingHom (Away r) (Away (DFunLike.coe f r))

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

Equations

• Eq (Localization.awayMap f r) (IsLocalization.Away.map (Localization.Away r) (Localization.Away (DFunLike.coe f r)) f r)

@[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 : AlgHom R A B) (a : A) : AlgHom R (Away a) (Away (DFunLike.coe f a))

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

Equations

• Eq (Localization.awayMapₐ f a) (IsLocalization.Away.mapₐ (Localization.Away a) (Localization.Away (DFunLike.coe f a)) f a)

theorem Localization.algebraMap_injective_of_span_eq_top {R : Type u_1} [CommSemiring R] (s : Set R) (span_eq : Eq (Ideal.span s) Top.top) : Function.Injective (DFunLike.coe (algebraMap R ((a : s.Elem) → Away a.val)))

theorem Localization.existsUnique_algebraMap_eq_of_span_eq_top {R : Type u_1} [CommSemiring R] (s : Set R) (span_eq : Eq (Ideal.span s) Top.top) (f : (a : s.Elem) → Away a.val) (h : ∀ (a b : s.Elem), Eq (DFunLike.coe (IsLocalization.Away.awayToAwayRight a.val b.val) (f a)) (DFunLike.coe (IsLocalization.Away.awayToAwayLeft b.val a.val) (f b))) : ExistsUnique fun (r : R) => ∀ (a : s.Elem), Eq (DFunLike.coe (algebraMap R (Away a.val)) r) (f a)

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

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 : Int) : B

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

Equations

• Eq (selfZPow x B m) (if x_1 : LE.le 0 m then HPow.hPow (DFunLike.coe (algebraMap R B) x) m.natAbs else IsLocalization.mk' B 1 (Submonoid.pow x m.natAbs))

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 : Int} (hn : LE.le 0 n) : Eq (selfZPow x B n) (HPow.hPow (DFunLike.coe (algebraMap R B) x) n.natAbs)

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 : Nat) : Eq (selfZPow x B d.cast) (HPow.hPow (DFunLike.coe (algebraMap R B) x) d)

theorem selfZPow_zero {R : Type u_1} [CommSemiring R] (x : R) (B : Type u_2) [CommSemiring B] [Algebra R B] [IsLocalization.Away x B] : Eq (selfZPow x B 0) 1

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 : Int} (hn : LT.lt n 0) : Eq (selfZPow x B n) (IsLocalization.mk' B 1 (Submonoid.pow x n.natAbs))

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 : Int} (hn : LE.le n 0) : Eq (selfZPow x B n) (IsLocalization.mk' B 1 (Submonoid.pow x n.natAbs))

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 : Nat) : Eq (selfZPow x B (Neg.neg d.cast)) (IsLocalization.mk' B 1 (Submonoid.pow x d))

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 : Nat} : Eq (selfZPow x B (HSub.hSub n.cast m.cast)) (IsLocalization.mk' B (HPow.hPow x n) (Submonoid.pow x m))

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 : Int} : Eq (selfZPow x B (HAdd.hAdd n m)) (HMul.hMul (selfZPow x B n) (selfZPow x B m))

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 : Int) : Eq (HMul.hMul (selfZPow x B d) (selfZPow x B (Neg.neg d))) 1

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 : Int) : Eq (HMul.hMul (selfZPow x B (Neg.neg d)) (selfZPow x B d)) 1

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 : Int) : Iff (Eq (HMul.hMul (selfZPow x B (HSub.hSub m d)) (IsLocalization.mk' B a 1)) b) (Eq (HMul.hMul (selfZPow x B m) (IsLocalization.mk' B a 1)) (HMul.hMul (selfZPow x B d) b))

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 : Ne b 0) (hx : Irreducible x) : Exists fun (a : R) => Exists fun (n : Int) => And (Not (Dvd.dvd x a)) (Eq (HMul.hMul (selfZPow x B n) (DFunLike.coe (algebraMap R B) a)) b)