Theorems · Theorem · group theory
sub_zero
∀ {G : Type u_3} [inst : SubNegZeroMonoid G] (a : G), a - 0 = a- Defined in
- Mathlib.Algebra.Group.Basic
- Cited by
- 938 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 44 definitions · uses propext
- Assumes
- SubNegZeroMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- add_zeroproof · cited by 2,707
- sub_eq_add_negproof · cited by 1,023
- neg_zeroproof · cited by 542
- SubNegZeroMonoidstatement and proof · cited by 13
Cited by938
Results whose statement or proof uses this declaration.
- norm_negproof · cited by 190
- Complex.ofReal_mulproof · cited by 180
- intervalIntegral.integral_of_leproof · cited by 83
- Real.exp_addproof · cited by 39
- MeasureTheory.integral_eq_lintegral_of_nonneg_aeproof · cited by 31
- Complex.re_ofReal_mulproof · cited by 20
- IsIdempotentElem.one_subproof · cited by 20
- NNReal.coe_subproof · cited by 19
- Real.cos_antiperiodicproof · cited by 16
- descPochhammer_succ_rightproof · cited by 14
- Complex.inv_reproof · cited by 13
- Seminorm.mem_ball_zeroproof · cited by 11
Showing the 200 most cited of 938.