Theorems · Theorem · number theory
Int.negOnePow_sub
∀ (n₁ n₂ : ℤ), (n₁ - n₂).negOnePow = n₁.negOnePow * n₂.negOnePow
- Defined in
- Mathlib.Algebra.Ring.NegOnePow
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 42 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
- sub_eq_add_negproof · cited by 1,023
- Int.negOnePowstatement and proof · cited by 156
- Int.negOnePow_addproof · cited by 25
- Int.negOnePow_negproof · cited by 13
Cited by4
Results whose statement or proof uses this declaration.
- Polynomial.Chebyshev.C_eval_neg_twoproof · cited by 0
- Polynomial.Chebyshev.U_eval_neg_oneproof · cited by 0
- Polynomial.Chebyshev.T_eval_neg_oneproof · cited by 0
- Polynomial.Chebyshev.S_eval_neg_twoproof · cited by 0