Theorems · Theorem · order theory
inv_nonneg_of_nonneg
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}, 0 ≤ a → 0 ≤ a⁻¹Alias of the reverse direction of inv_nonneg.
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- PartialOrderstatement and proof · cited by 6,410
- GroupWithZerostatement and proof · cited by 691
- PosMulReflectLTstatement and proof · cited by 278
- inv_nonnegproof · cited by 56
Cited by24
Results whose statement or proof uses this declaration.
- ProbabilityTheory.gaussianPDFReal_nonnegproof · cited by 6
- Real.ofDigitsTerm_nonnegproof · cited by 4
- PeriodPair.hasSumLocallyUniformly_weierstrassPExceptproof · cited by 4
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- AkraBazziRecurrence.GrowsPolynomially.invproof · cited by 3
- uniformContinuousOn_inv₀proof · cited by 2
- MeasureTheory.eLpNorm_smul_measure_of_ne_top'proof · cited by 2
- MeasureTheory.uniformIntegrable_of'proof · cited by 2
- tendsto_div_of_monotone_of_exists_subseq_tendsto_divproof · cited by 1
- ProbabilityTheory.strong_law_ae_of_measurableproof · cited by 1
- Orientation.abs_volumeForm_apply_of_pairwise_orthogonalproof · cited by 1
- ProbabilityTheory.strong_law_aux1proof · cited by 1