Theorems · Theorem · group theory
zero_sub
∀ {G : Type u_1} [inst : SubNegMonoid G] (a : G), 0 - a = -a- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 335 results in Mathlib
- Foundations
- Depth 8 from the axioms, rests on 38 definitions · uses no axioms
- Assumes
- SubNegMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SubNegMonoidstatement and proof · cited by 79
- neg_eq_zero_subproof · cited by 1
Cited by335
Results whose statement or proof uses this declaration.
- norm_negproof · cited by 190
- Complex.I_mul_Iproof · cited by 35
- vsub_vadd_eq_vsub_subproof · cited by 32
- hasSum_geometric_of_lt_oneproof · cited by 14
- bernoulli'_zeroproof · cited by 9
- AffineMap.lineMap_apply_one_subproof · cited by 8
- Polynomial.Chebyshev.T_derivative_eq_Uproof · cited by 7
- Polynomial.Chebyshev.U_neg_oneproof · cited by 7
- UpperHalfPlane.norm_exp_two_pi_I_lt_oneproof · cited by 7
- Sbtw.angle₁₂₃_eq_piproof · cited by 6
- Real.rpowIntegrand₀₁_eq_pow_divproof · cited by 6
- Function.Periodic.norm_qParamproof · cited by 6
Showing the 200 most cited of 335.