Theorems · Theorem · functional analysis
norm_neg
∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), ‖-a‖ = ‖a‖- Defined in
- Mathlib.Analysis.Normed.Group.Basic
- Cited by
- 190 results in Mathlib
- Foundations
- Depth 18 from the axioms, rests on 68 definitions · uses propext, Quot.sound
- Assumes
- SeminormedAddGroup
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.
- Realstatement · cited by 25,697
- Norm.normstatement and proof · cited by 5,413
- sub_zeroproof · cited by 938
- zero_subproof · cited by 335
- SeminormedAddGroupstatement and proof · cited by 331
- norm_sub_revproof · cited by 41
Cited by191
Results whose statement or proof uses this declaration.
- tendsto_zero_iff_norm_tendsto_zeroproof · cited by 29
- norm_sub_leproof · cited by 26
- nnnorm_negproof · cited by 13
- NormedAddGroup.nhds_zero_basis_norm_ltproof · cited by 7
- InnerProductGeometry.angle_neg_rightproof · cited by 7
- ExistsContDiffBumpBase.u_existsproof · cited by 5
- norm_sub_sqproof · cited by 5
- AddMonoidHomClass.isometry_iff_normproof · cited by 5
- PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExceptproof · cited by 4
- Complex.norm_log_sub_logTaylor_leproof · cited by 4
- Complex.ofReal_cpow_of_nonposproof · cited by 4
- MeasureTheory.convolution_eq_right'proof · cited by 4