Theorems · Theorem · ring theory
neg_pow
∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R) (n : ℕ), (-a) ^ n = (-1) ^ n * a ^ n- Defined in
- Mathlib.Algebra.Ring.Commute
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext
- Assumes
- MonoidHasDistribNeg
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.
- Monoidstatement and proof · cited by 3,887
- HasDistribNegstatement and proof · cited by 114
- neg_one_mulproof · cited by 61
- Commute.mul_powproof · cited by 22
- Commute.neg_one_leftproof · cited by 3
Cited by14
Results whose statement or proof uses this declaration.
- IsNilpotent.negproof · cited by 5
- Complex.norm_log_sub_logTaylor_leproof · cited by 4
- Commute.pow_dvd_pow_of_sub_pow_eq_zeroproof · cited by 3
- Complex.hasSum_sinhproof · cited by 2
- GaloisField.finrankproof · cited by 2
- Polynomial.bernoulli_comp_one_sub_Xproof · cited by 2
- fermatLastTheoremWith_nat_int_rat_tfaeproof · cited by 2
- minpoly.natSepDegree_eq_one_iff_eq_X_sub_C_powproof · cited by 1
- Polynomial.factorial_mul_shiftedLegendre_eqproof · cited by 1
- EisensteinSeries.qExpansion_identityproof · cited by 1
- Quaternion.expSeries_even_of_imaginaryproof · cited by 1
- Quaternion.expSeries_odd_of_imaginaryproof · cited by 1