Theorems · Theorem · order theory
zpow_nonneg
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
[ZeroLEOneClass G₀], 0 ≤ a → ∀ (n : ℤ), 0 ≤ a ^ n- Cited by
- 7 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.
Cites8
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
- ZeroLEOneClassstatement and proof · cited by 304
- PosMulReflectLTstatement and proof · cited by 278
- zpow_natCastproof · cited by 271
- zpow_negproof · cited by 198
- pow_nonnegproof · cited by 141
- inv_nonnegproof · cited by 56
Cited by7
Results whose statement or proof uses this declaration.
- zpow_right_mono₀proof · cited by 4
- zpow_right_anti₀proof · cited by 3
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- Odd.zpow_neg_iffproof · cited by 3
- padicNorm.nonnegproof · cited by 1
- Nonneg.mk_zpowstatement · cited by 0
- Real.toNNReal_zpowproof · cited by 0