Theorems · Theorem · commutative algebra
selfZPow_mul_neg
∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
[inst_3 : IsLocalization.Away x B] (d : ℤ), selfZPow x B d * selfZPow x B (-d) = 1- Cited by
- 3 results in Mathlib
- Foundations
- Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites21
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- Algebra.algebraMapproof · cited by 4,706
- LT.lt.leproof · cited by 2,189
- le_of_ltproof · cited by 1,175
- neg_negproof · cited by 960
- map_oneproof · cited by 861
- map_powproof · cited by 503
- Submonoid.powersproof · cited by 408
- IsLocalization.mk'proof · cited by 218
- IsLocalization.Awaystatement and proof · cited by 218
Cited by3
Results whose statement or proof uses this declaration.
- Ideal.isPrincipal_of_isPrincipal_isLocalizationAway_of_primeproof · cited by 2
- selfZPow_pow_subproof · cited by 1
- selfZPow_neg_mulproof · cited by 1