Theorems · Theorem · order theory
zpow_pos
∀ {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
- 22 results in Mathlib
- Foundations
- Depth 21 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
- pow_posproof · cited by 292
- PosMulReflectLTstatement and proof · cited by 278
- zpow_natCastproof · cited by 271
- zpow_negproof · cited by 198
- inv_posproof · cited by 124
Cited by24
Results whose statement or proof uses this declaration.
- zpow_right_strictMono₀proof · cited by 8
- zpow_right_strictAnti₀proof · cited by 7
- PadicInt.exists_pow_neg_ltproof · cited by 6
- WithZeroMulInt.toNNReal_strictMonoproof · cited by 4
- PeriodPair.summable_weierstrassPExceptSummandproof · cited by 3
- SchwartzMap.isBigO_cocompact_rpowproof · cited by 3
- Padic.norm_le_pow_iff_norm_lt_pow_add_oneproof · cited by 2
- Int.zpowLogGistatement · cited by 2
- Seminorm.rescale_to_shell_zpowproof · cited by 2
- Int.clogZPowGistatement · cited by 2
- ModularFormClass.qExpansion_isBigOproof · cited by 1
- SchwartzMap.isBigO_cocompact_zpow_neg_natproof · cited by 1