Theorems · Theorem · number theory
Int.negOnePow_neg
∀ (n : ℤ), (-n).negOnePow = n.negOnePow
- Defined in
- Mathlib.Algebra.Ring.NegOnePow
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 41 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Unitsstatement · cited by 2,804
- inv_oneproof · cited by 301
- zpow_negproof · cited by 198
- Int.negOnePowstatement · cited by 156
- inv_negproof · cited by 42
Cited by13
Results whose statement or proof uses this declaration.
- Int.negOnePow_subproof · cited by 4
- Polynomial.Chebyshev.T_eval_negproof · cited by 4
- Function.Antiperiodic.sub_zsmul_eqproof · cited by 2
- CochainComplex.mappingCone.δ_liftCochainproof · cited by 1
- Polynomial.Chebyshev.sumZeroes_T_of_not_dvdproof · cited by 1
- PowerSeries.WithPiTopology.hasSum_pow_pentagonal_sub_pentagonalSeriesproof · cited by 1
- Int.negOnePow_absproof · cited by 0
- Polynomial.Chebyshev.S_eval_neg_twoproof · cited by 0
- CochainComplex.IsKInjective.eq_δ_of_cocycle'proof · cited by 0
- Polynomial.Chebyshev.U_eval_neg_oneproof · cited by 0
- CategoryTheory.Triangulated.TStructure.exists_triangleproof · cited by 0
- CochainComplex.mappingCocone.δ_descCochainproof · cited by 0