Mathlib Map

Theorems · Definition · order theory

NegPart.negPart

{α : Type u_1} → [self : NegPart α] → α → α

The negative part of an element a.

Defined in
Mathlib.Algebra.Notation
Cited by
107 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Assumes
NegPart
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

ValueDistribution.logCounting · cited by 45ValueDistribution.logCoun…negPart_of_nonpos · cited by 11negPart_of_nonposCFC.posPart_sub_negPart · cited by 10CFC.posPart_sub_negPartCFC.negPart_def · cited by 9CFC.negPart_defposPart_sub_negPart · cited by 9posPart_sub_negPartcontinuous_negPart · cited by 9continuous_negPartnegPart_nonneg · cited by 7negPart_nonnegCStarAlgebra.nonneg_TFAE · cited by 6CStarAlgebra.nonneg_TFAEnegPart_def · cited by 6negPart_defCFC.negPart_nonneg · cited by 5CFC.negPart_nonnegCFC.posPart_neg · cited by 4CFC.posPart_negnegPart_eq_zero · cited by 4negPart_eq_zeroCStarAlgebra.nonneg_iff_eq_star_mul_self · cited by 3CStarAlgebra.nonneg_iff_e…posPart_add_negPart · cited by 3posPart_add_negPartnegPart_eq_neg · cited by 3negPart_eq_negNegPart · cited by 2NegPartNegPart.negPartCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • NegPartstatement and proof · cited by 2

Cited by108

Results whose statement or proof uses this declaration.