Mathlib Map

Theorems · Definition · order theory

PosPart.posPart

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

The positive part of an element a.

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

Around this declaration

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

ValueDistribution.logCounting · cited by 45ValueDistribution.logCoun…posPart_zero · cited by 12posPart_zerocontinuous_posPart · cited by 12continuous_posPartCFC.posPart_sub_negPart · cited by 10CFC.posPart_sub_negPartposPart_sub_negPart · cited by 9posPart_sub_negPartCFC.posPart_def · cited by 9CFC.posPart_defposPart_nonneg · cited by 8posPart_nonnegCStarAlgebra.nonneg_TFAE · cited by 6CStarAlgebra.nonneg_TFAEposPart_def · cited by 6posPart_defposPart_eq_self · cited by 6posPart_eq_selfCFC.posPart_nonneg · cited by 5CFC.posPart_nonnegCFC.posPart_neg · cited by 4CFC.posPart_negCStarAlgebra.nonneg_iff_eq_star_mul_self · cited by 3CStarAlgebra.nonneg_iff_e…CStarAlgebra.norm_posPart_le · cited by 3CStarAlgebra.norm_posPart…posPart_add_negPart · cited by 3posPart_add_negPartPosPart · cited by 2PosPartPosPart.posPartCITED BYCITES

Cites1

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

  • PosPartstatement and proof · cited by 2

Cited by114

Results whose statement or proof uses this declaration.