Theorems · Theorem · order theory
SignType.coe_neg
∀ {α : Type u_2} [inst : One α] [inst_1 : SubtractionMonoid α] (s : SignType), ↑(-s) = -↑s- Defined in
- Mathlib.Data.Sign.Defs
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- OneSubtractionMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- neg_negproof · cited by 960
- neg_zeroproof · cited by 542
- SignTypestatement and proof · cited by 318
- SubtractionMonoidstatement and proof · cited by 208
- SignType.caststatement and proof · cited by 76
- SignType.casesOnproof · cited by 14
Cited by19
Results whose statement or proof uses this declaration.
- Affine.Simplex.ExcenterExists.dist_excenterproof · cited by 6
- self_mul_signproof · cited by 3
- hasStrictDerivAt_absproof · cited by 2
- sign_mul_absproof · cited by 2
- signedDist_negproof · cited by 1
- NormedSpace.normalize_smulproof · cited by 1
- Matrix.IsTotallyUnimodular.fromRows_unitlikeproof · cited by 1
- HurwitzZeta.hasSum_nat_hurwitzZetaOddproof · cited by 1
- DivisibleHull.qsmul_of_nonposproof · cited by 1
- Int.sign_eq_signproof · cited by 1
- QuadraticForm.equivalent_one_neg_one_weighted_sum_squaredproof · cited by 0
- QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squaredproof · cited by 0