Basic

📁 Source: Mathlib/RingTheory/Localization/Away/Basic.lean

Statistics

Metric	Count
Definitions `awayToAwayLeft`, `awayToAwayRight`, `invSelf`, `map`, `mapₐ`, `sec`, `atOne`, `atUnit`, `awayLift`, `awayMap`, `awayMapₐ`, `selfZPow`	12
Theorems `algebraMap_isUnit`, `algebraMap_isUnit_iff`, `algebraMap_pow_isUnit`, `algebraMap_surjective_of_isIdempotentElem`, `associated_sec_fst`, `awayToAwayLeft_eq`, `awayToAwayRight_eq`, `commutes`, `exists_of_eq`, `iff_of_associated`, `instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap`, `instHMulAwayCoeRingHomAlgebraMap`, `instHMulAwayCoeRingHomAlgebraMap_1`, `instMapRingHomPowersOfCoe`, `isUnit_of_dvd`, `lift_comp`, `lift_eq`, `map_injective_iff`, `map_surjective_iff`, `mapₐ_apply`, `mapₐ_injective_of_injective`, `mapₐ_surjective_of_surjective`, `mk`, `mul`, `mul'`, `mul_invSelf`, `mul_of_associated`, `mul_of_isUnit`, `mul_of_isUnit'`, `of_associated`, `of_surjective`, `of_surjective_of_isScalarTower`, `sec_spec`, `surj`, `away_fst`, `away_of_isIdempotentElem`, `away_of_isIdempotentElem_of_mul`, `away_of_isUnit_of_bijective`, `away_snd`, `algebraMap_injective_of_span_eq_top`, `awayLift_mk`, `awayMap_awayMap_surjective`, `awayMap_bijective_of_dvd`, `awayMap_injective_iff`, `awayMap_injective_of_dvd`, `awayMap_surjective_iff`, `awayMap_surjective_of_dvd`, `existsUnique_algebraMap_eq_of_span_eq_top`, `exists_reduced_fraction'`, `selfZPow_add`, `selfZPow_mul_neg`, `selfZPow_natCast`, `selfZPow_neg_mul`, `selfZPow_neg_natCast`, `selfZPow_of_neg`, `selfZPow_of_nonneg`, `selfZPow_of_nonpos`, `selfZPow_pow_sub`, `selfZPow_sub_natCast`, `selfZPow_zero`	60
Total	72

IsLocalization

Definitions

Name	Category	Theorems
`atOne` 📖	CompOp	—
`atUnit` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`away_fst` 📖	mathematical	—	`Away` `Prod.instCommSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHom.toAlgebra` `RingHom.fst`	—	`away_of_isIdempotentElem_of_mul` `mul_one` `MulZeroClass.mul_zero` `one_mul` `MulZeroClass.zero_mul` `Prod.fst_surjective` `Zero.instNonempty`
`away_of_isIdempotentElem` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `Ideal.span` `Set` `Set.instSingletonSet` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `DFunLike.coe`	`Away`	—	`RingHom.instRingHomClass` `away_of_isIdempotentElem_of_mul` `sub_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `RingHom.mem_ker` `IsIdempotentElem.ker_toSpanSingleton_eq_span` `LinearMap.mem_ker` `LinearMap.toSpanSingleton_apply` `sub_smul` `mul_comm`
`away_of_isIdempotentElem_of_mul` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	`Away`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `RingHom.map_one` `mul_one` `one_pow` `map_one` `MonoidHomClass.toOneHomClass` `Submonoid.mem_powers`
`away_of_isUnit_of_bijective` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Function.Bijective` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`Away`	—	`RingHom.isUnit_map` `IsUnit.pow` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `mul_one`
`away_snd` 📖	mathematical	—	`Away` `Prod.instCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.toAlgebra` `RingHom.snd`	—	`away_of_isIdempotentElem_of_mul` `MulZeroClass.mul_zero` `mul_one` `MulZeroClass.zero_mul` `one_mul` `Prod.snd_surjective` `Zero.instNonempty`

IsLocalization.Away

Definitions

Name	Category	Theorems
`awayToAwayLeft` 📖	CompOp	1 math math: `awayToAwayLeft_eq`
`awayToAwayRight` 📖	CompOp	3 math math: `awayToAwayRight_eq`, `AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE_assoc`, `AlgebraicGeometry.basicOpenIsoSpecAway_inv_homOfLE`
`invSelf` 📖	CompOp	4 math math: `Algebra.Generators.compLocalizationAwayAlgHom_X_inl`, `mvPolynomialQuotientEquiv_apply`, `mul_invSelf`, `Algebra.Generators.localizationAway_val`
`map` 📖	CompOp	8 math math: `RingHom.localization_away_map_finite`, `map_injective_iff`, `map_surjective_iff`, `RingHom.localization_away_map_finiteType`, `RingHom.RespectsIso.isLocalization_away_iff`, `mapₐ_apply`, `AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map`, `AlgebraicGeometry.IsAffineOpen.appLE_eq_away_map`
`mapₐ` 📖	CompOp	3 math math: `mapₐ_surjective_of_surjective`, `mapₐ_injective_of_injective`, `mapₐ_apply`
`sec` 📖	CompOp	3 math math: `sec_spec`, `Algebra.Generators.localizationAway_σ`, `associated_sec_fst`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_isUnit` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsLocalization.map_units` `pow_one`
`algebraMap_isUnit_iff` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Monoid.toNatPow`	—	`IsLocalization.algebraMap_isUnit_iff`
`algebraMap_pow_isUnit` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Monoid.toNatPow` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsUnit.pow` `IsLocalization.map_units` `pow_one`
`algebraMap_surjective_of_isIdempotentElem` 📖	mathematical	`IsIdempotentElem` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	`DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`IsLocalization.exists_mk'_eq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `IsIdempotentElem.pow_succ_eq` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `IsLocalization.eq_iff_exists`
`associated_sec_fst` 📖	mathematical	—	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `sec`	—	`sec_spec` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `associated_mul_unit_left` `IsUnit.pow` `algebraMap_isUnit`
`awayToAwayLeft_eq` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `awayToAwayLeft` `algebraMap`	—	`lift_eq`
`awayToAwayRight_eq` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `awayToAwayRight` `algebraMap`	—	`lift_eq`
`commutes` 📖	mathematical	—	`IsLocalization.Away` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	—	`Submonoid.ext` `Algebra.algebraMapSubmonoid_powers` `IsLocalization.commutes` `instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap`
`exists_of_eq` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsLocalization.exists_of_eq`
`iff_of_associated` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsLocalization.Away`	—	`of_associated` `Associated.symm`
`instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap` 📖	mathematical	—	`IsLocalization` `Algebra.algebraMapSubmonoid` `CommSemiring.toSemiring` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Algebra.algebraMapSubmonoid_powers`
`instHMulAwayCoeRingHomAlgebraMap` 📖	mathematical	—	`IsLocalization.Away` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Localization.Away` `CommSemiring.toCommMonoid` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `OreLocalization.instCommSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra`	—	`mul` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization`
`instHMulAwayCoeRingHomAlgebraMap_1` 📖	mathematical	—	`IsLocalization.Away` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Localization.Away` `CommSemiring.toCommMonoid` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `OreLocalization.instCommSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `OreLocalization.instAlgebra`	—	`mul'` `OreLocalization.instIsScalarTower` `IsScalarTower.right` `Localization.isLocalization`
`instMapRingHomPowersOfCoe` 📖	mathematical	—	`IsLocalization` `Submonoid.map` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.powers`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.map_powers`
`isUnit_of_dvd` 📖	mathematical	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`isUnit_of_dvd_unit` `map_dvd` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `algebraMap_isUnit`
`lift_comp` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`RingHom.comp` `lift` `algebraMap`	—	`IsLocalization.lift_comp`
`lift_eq` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`lift` `algebraMap`	—	`IsLocalization.lift_eq`
`map_injective_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Function.Surjective.forall` `IsLocalization.mk'_surjective` `IsLocalization.map_mk'` `One.instNonempty` `pow_zero` `one_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `pow_add` `mul_assoc`
`map_surjective_iff` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `map` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Function.Surjective.exists` `IsLocalization.mk'_surjective` `IsLocalization.map_mk'` `Function.Surjective.forall` `IsLocalization.eq_iff_exists` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `pow_add` `zero_add` `map_mul` `map_pow` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one` `Mathlib.Tactic.RingNF.mul_assoc_rev` `add_zero`
`mapₐ_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike` `mapₐ` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `map` `AlgHom.toRingHom`	—	—
`mapₐ_injective_of_injective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike`	`mapₐ`	—	`IsLocalization.map_injective_of_injective` `instMapRingHomPowersOfCoe`
`mapₐ_surjective_of_surjective` 📖	mathematical	`DFunLike.coe` `AlgHom` `CommSemiring.toSemiring` `AlgHom.funLike`	`mapₐ`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.map_powers` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `IsLocalization.map_surjective_of_surjective`
`mk` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow`	`IsLocalization.Away`	—	`map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsUnit.pow`
`mul` 📖	mathematical	—	`IsLocalization.Away` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`IsScalarTower.algebraMap_apply` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `instIsDedekindFiniteMonoid` `algebraMap_isUnit` `IsUnit.map` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `surj` `pow_add` `mul_pow` `map_pow` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `exists_of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add`
`mul'` 📖	mathematical	—	`IsLocalization.Away` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`mul` `mul_comm`
`mul_invSelf` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `invSelf` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`IsLocalization.mk'_one` `IsLocalization.mk'_mul_mk'_eq_one`
`mul_of_associated` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`IsLocalization.Away` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommRing.toCommSemiring`	—	`iff_of_associated` `mul'`
`mul_of_isUnit` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`IsLocalization.Away` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`IsLocalization.away_of_isUnit_of_bijective` `Function.bijective_id` `mul'` `IsScalarTower.right`
`mul_of_isUnit'` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	`IsLocalization.Away` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring`	—	`IsLocalization.away_of_isUnit_of_bijective` `Function.bijective_id` `mul` `IsScalarTower.right`
`of_associated` 📖	mathematical	`Associated` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`IsLocalization.Away`	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `instIsDedekindFiniteMonoid` `algebraMap_isUnit` `IsUnit.map` `Units.isUnit` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `surj` `mul_pow` `map_pow` `exists_of_eq` `mul_comm` `mul_assoc`
`of_surjective` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Algebra.id` `Monoid.toNatPow` `RingHom.ker` `RingHom.instRingHomClass` `Bot.bot` `Submodule.instBot`	`IsLocalization.Away`	—	`Algebra.to_smulCommClass` `RingHom.instRingHomClass` `pow_zero` `mul_one` `sub_eq_zero` `mul_sub` `map_sub` `RingHomClass.toAddMonoidHomClass` `sub_self`
`of_surjective_of_isScalarTower` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.instFunLike` `algebraMap` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `Submodule.instAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Submodule.pointwiseDistribMulAction` `Module.toDistribMulAction` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.to_smulCommClass` `Algebra.id` `Monoid.toNatPow` `RingHom.ker` `RingHom.instRingHomClass`	`IsLocalization.Away`	—	`Algebra.to_smulCommClass` `RingHom.instRingHomClass` `of_surjective` `IsScalarTower.algebraMap_apply` `Ideal.map_comap_of_surjective` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Ideal.map_pointwise_smul` `RingHom.comap_ker` `IsScalarTower.algebraMap_eq` `Ideal.map_le_iff_le_comap` `RingHom.ker_eq_comap_bot`
`sec_spec` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `sec`	—	—
`surj` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `algebraMap`	—	`IsLocalization.surj` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`

Localization

Definitions

Name	Category	Theorems
`awayLift` 📖	CompOp	2 math math: `HomogeneousLocalization.val_awayMap`, `awayLift_mk`
`awayMap` 📖	CompOp	8 math math: `Algebra.QuasiFiniteAt.exists_fg_and_exists_notMem_and_awayMap_bijective`, `awayMap_surjective_iff`, `exists_awayMap_bijective_of_residueField_surjective`, `exists_awayMap_injective_of_localRingHom_injective`, `RingHom.RespectsIso.isLocalization_away_iff`, `awayMap_injective_iff`, `exists_awayMap_bijective_of_localRingHom_bijective`, `Algebra.ZariskisMainProperty.exists_fg_and_exists_notMem_and_awayMap_bijective`
`awayMapₐ` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_injective_of_span_eq_top` 📖	mathematical	`Ideal.span` `CommSemiring.toSemiring` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`DFunLike.coe` `RingHom` `Pi.semiring` `Set.Elem` `Away` `CommSemiring.toCommMonoid` `Set` `Set.instMembership` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `RingHom.instFunLike` `algebraMap` `Pi.algebra` `OreLocalization.instAlgebra` `Algebra.id`	—	`Ideal.exists_disjoint_powers_of_span_eq_top` `IsLocalization.eq_iff_exists` `isLocalization` `Set.disjoint_left` `one_mul` `Ideal.eq_top_iff_one`
`awayLift_mk` 📖	mathematical	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`Away` `CommSemiring.toCommMonoid` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `awayLift` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulOne.toOne` `isUnit_iff_exists_inv` `instIsDedekindFiniteMonoid` `Submonoid` `SetLike.instMembership` `Submonoid.instSetLike` `Monoid.toNatPow`	—	`isUnit_iff_exists_inv` `instIsDedekindFiniteMonoid` `Submonoid.instSubmonoidClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `isLocalization` `mk_eq_mk'` `IsLocalization.lift_mk'` `Units.coe_liftRight` `map_pow` `mul_assoc` `mul_comm` `one_pow` `mul_one`
`awayMap_awayMap_surjective` 📖	mathematical	`Away` `CommSemiring.toCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `awayMap`	`OreLocalization.instCommSemiring` `algebraMap` `OreLocalization.instAlgebra` `Algebra.id`	—	`awayMap_surjective_iff` `zero_add` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `pow_add` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `isLocalization` `IsLocalization.map_eq` `Function.Surjective.exists` `IsLocalization.mk'_surjective` `IsLocalization.map_mk'` `Function.Surjective.forall` `IsLocalization.mul_mk'_eq_mk'_of_mul` `IsLocalization.eq_iff_exists`
`awayMap_bijective_of_dvd` 📖	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Function.Bijective` `Away` `CommSemiring.toCommMonoid` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `awayMap`	—	—	`awayMap_injective_of_dvd` `awayMap_surjective_of_dvd`
`awayMap_injective_iff` 📖	mathematical	—	`Away` `CommSemiring.toCommMonoid` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `awayMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`IsLocalization.Away.map_injective_iff`
`awayMap_injective_of_dvd` 📖	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Away` `CommSemiring.toCommMonoid` `CommRing.toCommSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `awayMap`	—	—	`mul_pow` `mul_assoc` `mul_left_comm` `MulZeroClass.mul_zero`
`awayMap_surjective_iff` 📖	mathematical	—	`Away` `CommSemiring.toCommMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `awayMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`IsLocalization.Away.map_surjective_iff`
`awayMap_surjective_of_dvd` 📖	—	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `CommSemiring.toNonUnitalCommSemiring` `Away` `CommSemiring.toCommMonoid` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `OreLocalization.instSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `awayMap`	—	—	`map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `mul_left_comm` `mul_pow` `mul_assoc`
`existsUnique_algebraMap_eq_of_span_eq_top` 📖	mathematical	`Ideal.span` `CommSemiring.toSemiring` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `RingHom` `Away` `CommSemiring.toCommMonoid` `Set` `Set.instMembership` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `OreLocalization.instCommSemiring` `Submonoid.powers` `CommMonoid.toMonoid` `OreLocalization.oreSetComm` `RingHom.instFunLike` `IsLocalization.Away.awayToAwayRight` `OreLocalization.instAlgebra` `Algebra.id` `isLocalization` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsLocalization.Away.awayToAwayLeft`	`ExistsUnique`	—	`isLocalization` `Ideal.eq_top_iff_one` `existsUnique_of_exists_of_unique` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `mul_left_comm` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `pow_add` `Finset.le_sup` `Finset.mem_attach` `IsLocalization.Away.exists_of_eq` `IsLocalization.Away.awayToAwayRight_eq` `IsLocalization.Away.awayToAwayLeft_eq` `mul_assoc` `mul_comm` `Finset.mem_product` `Finset.mk_mem_product` `mul_mul_mul_comm` `mul_pow` `Submodule.mem_span_range_iff_exists_fun` `Ideal.span_pow_eq_top` `Set.image_eq_range` `IsUnit.pow` `IsLocalization.Away.algebraMap_isUnit` `Finset.sum_mul` `Finset.sum_congr` `smul_eq_mul` `mul_one` `IsLocalization.Away.surj` `algebraMap_injective_of_span_eq_top` `Submodule.mem_span_finite_of_mem_span` `Set.insert_subset` `Ideal.span_mono` `Finset.coe_insert`

(root)

Definitions

Name	Category	Theorems
`selfZPow` 📖	CompOp	12 math math: `selfZPow_of_nonpos`, `selfZPow_zero`, `selfZPow_pow_sub`, `selfZPow_neg_mul`, `selfZPow_of_neg`, `selfZPow_natCast`, `selfZPow_sub_natCast`, `selfZPow_neg_natCast`, `selfZPow_mul_neg`, `selfZPow_of_nonneg`, `exists_reduced_fraction'`, `selfZPow_add`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_reduced_fraction'` 📖	mathematical	`Irreducible` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `selfZPow` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`IsLocalization.surj` `Submonoid.mem_powers_iff` `Function.mt` `injective_iff_map_eq_zero'` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `IsLocalization.injective` `powers_le_nonZeroDivisors_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `Irreducible.ne_zero` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `mul_ne_zero` `IsLocalization.isDomain_of_le_nonZeroDivisors` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsLocalization.to_map_ne_zero_of_mem_nonZeroDivisors` `IsDomain.toNontrivial` `mem_nonZeroDivisors_iff_ne_zero` `WfDvdMonoid.max_power_factor` `IsLocalization.mk'_one` `selfZPow_pow_sub` `selfZPow_natCast` `mul_comm` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`selfZPow_add` 📖	mathematical	—	`selfZPow` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`le_or_gt` `selfZPow_of_nonneg` `add_nonneg` `Int.instAddLeftMono` `pow_add` `LT.lt.le` `sub_neg_eq_add` `selfZPow_of_neg` `selfZPow_sub_natCast` `IsLocalization.mk'_eq_mul_mk'_one` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `add_comm` `mul_comm` `add_neg` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsLocalization.mk'_mul` `one_mul`
`selfZPow_mul_neg` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `selfZPow` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`selfZPow_of_nonpos` `selfZPow_of_nonneg` `nonneg_of_neg_nonpos` `Int.instAddLeftMono` `neg_neg` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `Submonoid.pow_apply` `IsLocalization.mk'_spec` `map_one` `MonoidHomClass.toOneHomClass` `LT.lt.le` `nonpos_of_neg_nonneg` `le_of_lt`
`selfZPow_natCast` 📖	mathematical	—	`selfZPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	`selfZPow_of_nonneg`
`selfZPow_neg_mul` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `selfZPow` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`mul_comm` `selfZPow_mul_neg`
`selfZPow_neg_natCast` 📖	mathematical	—	`selfZPow` `IsLocalization.mk'` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Submonoid.pow`	—	`selfZPow_of_nonpos` `neg_nonpos` `Int.instAddLeftMono` `IsLocalization.mk'.congr_simp`
`selfZPow_of_neg` 📖	mathematical	—	`selfZPow` `IsLocalization.mk'` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Submonoid.pow`	—	`LT.lt.not_ge`
`selfZPow_of_nonneg` 📖	mathematical	—	`selfZPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `algebraMap`	—	—
`selfZPow_of_nonpos` 📖	mathematical	—	`selfZPow` `IsLocalization.mk'` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `Submonoid.pow`	—	`selfZPow.congr_simp` `selfZPow_zero` `pow_zero` `IsLocalization.mk'.congr_simp` `IsLocalization.mk'_self` `selfZPow_of_neg` `lt_of_le_of_ne`
`selfZPow_pow_sub` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `selfZPow` `IsLocalization.mk'` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.one`	—	`sub_eq_add_neg` `selfZPow_add` `mul_assoc` `mul_comm` `mul_one` `selfZPow_neg_mul` `selfZPow_mul_neg`
`selfZPow_sub_natCast` 📖	mathematical	—	`selfZPow` `IsLocalization.mk'` `Submonoid.powers` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Monoid.toNatPow` `Submonoid.pow`	—	`IsLocalization.eq_mk'_iff_mul_eq` `Submonoid.pow_apply` `selfZPow_natCast` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `pow_add` `neg_sub` `LT.lt.le` `selfZPow_neg_natCast` `IsLocalization.mk'_eq_iff_eq` `mul_one`
`selfZPow_zero` 📖	mathematical	—	`selfZPow` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring`	—	`selfZPow_of_nonneg` `le_rfl` `pow_zero`

---

← Back to Index