Real

📁 Source: Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Statistics

Metric	Count
Definitions evalRPow, proveIsNatRPowIsNNRat, evalRpow, evalRpowZero, instPow, rpow	6
Theorems abs_cpow_inv_two_im, cpow_inv_two_im_eq_neg_sqrt, cpow_inv_two_im_eq_sqrt, cpow_inv_two_re, cpow_mul_ofReal_nonneg, cpow_ofReal, cpow_ofReal_im, cpow_ofReal_re, inv_natCast_cpow_ofReal_pos, norm_cpow_eq_rpow_re_of_nonneg, norm_cpow_eq_rpow_re_of_pos, norm_cpow_inv_nat, norm_cpow_le, norm_cpow_of_imp, norm_cpow_of_ne_zero, norm_cpow_real, norm_log_natCast_le_rpow_div, norm_natCast_cpow_le_norm_natCast_cpow_iff, norm_natCast_cpow_le_norm_natCast_cpow_of_pos, norm_natCast_cpow_of_pos, norm_natCast_cpow_of_re_ne_zero, norm_natCast_cpow_pos_of_pos, norm_ofReal_cpow_eventually_eq_atTop, norm_prime_cpow_le_one_half, ofReal_cpow, ofReal_cpow_of_nonpos, one_sub_prime_cpow_ne_zero, rpow_const, rpow_eq_inv_pow, rpow_isNNRat, rpow_eq_pow, rpow_isNNRat, isInt_rpow_neg, isInt_rpow_pos, isNNRat_rpow_neg, isNNRat_rpow_pos, isNat_rpow_neg, isNat_rpow_pos, isRat_rpow_neg, isRat_rpow_pos, rpow_isRat_eq_inv_rpow, abs_log_mul_self_rpow_lt, abs_rpow_le_abs_rpow, abs_rpow_le_exp_log_mul, abs_rpow_of_nonneg, antitoneOn_rpow_Ioi_of_exponent_nonpos, antitone_rpow_of_base_le_one, div_rpow, eq_rpow_inv, eq_zero_rpow_iff, exp_mul, exp_one_pow, exp_one_rpow, inv_rpow, le_log_of_pow_le, le_log_of_rpow_le, le_log_of_zpow_le, le_pow_iff_log_le, le_pow_of_log_le, le_rpow_add, le_rpow_iff_log_le, le_rpow_inv_iff_of_neg, le_rpow_inv_iff_of_pos, le_rpow_of_log_le, le_zpow_iff_log_le, le_zpow_of_log_le, log_le_rpow_div, log_natCast_le_rpow_div, log_rpow, lt_log_of_pow_lt, lt_log_of_rpow_lt, lt_log_of_zpow_lt, lt_pow_iff_log_lt, lt_pow_of_log_lt, lt_rpow_iff_log_lt, lt_rpow_inv_iff_of_neg, lt_rpow_inv_iff_of_pos, lt_rpow_of_log_lt, lt_zpow_iff_log_lt, lt_zpow_of_log_lt, monotoneOn_rpow_Ici_of_exponent_nonneg, monotone_rpow_of_base_ge_one, mul_log_eq_log_iff, mul_rpow, norm_rpow_of_nonneg, one_le_rpow, one_le_rpow_of_pos_of_le_one_of_nonpos, one_lt_rpow, one_lt_rpow_iff, one_lt_rpow_iff_of_pos, one_lt_rpow_of_pos_of_lt_one_of_neg, one_rpow, pi_rpow_zero, pow_le_iff_le_log, pow_le_of_le_log, pow_lt_iff_lt_log, pow_lt_of_lt_log, pow_rpow_inv_natCast, rpow_add, rpow_add', rpow_add_intCast, rpow_add_intCast', rpow_add_natCast, rpow_add_natCast', rpow_add_of_nonneg, rpow_add_one, rpow_add_one', rpow_def, rpow_def_of_neg, rpow_def_of_nonneg, rpow_def_of_nonpos, rpow_def_of_pos, rpow_div_two_eq_sqrt, rpow_eq_pow, rpow_eq_zero, rpow_eq_zero_iff_of_nonneg, rpow_intCast, rpow_intCast_mul, rpow_inv_eq, rpow_inv_le_iff_of_neg, rpow_inv_le_iff_of_pos, rpow_inv_log, rpow_inv_log_le_exp_one, rpow_inv_lt_iff_of_neg, rpow_inv_lt_iff_of_pos, rpow_inv_natCast_pow, rpow_inv_rpow, rpow_le_iff_le_log, rpow_le_of_le_log, rpow_le_one, rpow_le_one_iff_of_pos, rpow_le_one_of_one_le_of_nonpos, rpow_le_rpow, rpow_le_rpow_iff, rpow_le_rpow_iff_of_neg, rpow_le_rpow_left_iff, rpow_le_rpow_left_iff_of_base_lt_one, rpow_le_rpow_of_exponent_ge, rpow_le_rpow_of_exponent_ge', rpow_le_rpow_of_exponent_ge_of_imp, rpow_le_rpow_of_exponent_le, rpow_le_rpow_of_exponent_le_or_ge, rpow_le_rpow_of_exponent_nonpos, rpow_le_rpow_of_nonpos, rpow_le_self_of_le_one, rpow_le_self_of_one_le, rpow_left_inj, rpow_left_injOn, rpow_lt_iff_lt_log, rpow_lt_of_lt_log, rpow_lt_one, rpow_lt_one_iff, rpow_lt_one_iff', rpow_lt_one_iff_of_pos, rpow_lt_one_of_one_lt_of_neg, rpow_lt_rpow, rpow_lt_rpow_iff, rpow_lt_rpow_iff_of_neg, rpow_lt_rpow_left_iff, rpow_lt_rpow_left_iff_of_base_lt_one, rpow_lt_rpow_of_exponent_gt, rpow_lt_rpow_of_exponent_lt, rpow_lt_rpow_of_exponent_neg, rpow_lt_rpow_of_neg, rpow_lt_self_of_lt_one, rpow_lt_self_of_one_lt, rpow_max, rpow_mul, rpow_mul_intCast, rpow_mul_natCast, rpow_natCast, rpow_natCast_mul, rpow_ne_zero, rpow_neg, rpow_neg_eq_inv_rpow, rpow_neg_natCast, rpow_neg_ofNat, rpow_neg_one, rpow_nonneg, rpow_ofNat, rpow_of_add_eq, rpow_one, rpow_one_add', rpow_one_sub', rpow_pos_of_pos, rpow_pow_comm, rpow_right_inj, rpow_rpow_inv, rpow_sub, rpow_sub', rpow_sub_intCast, rpow_sub_intCast', rpow_sub_natCast, rpow_sub_natCast', rpow_sub_one, rpow_sub_one', rpow_sum_of_nonneg, rpow_sum_of_pos, rpow_two, rpow_zero, rpow_zero_pos, rpow_zpow_comm, self_le_rpow_of_le_one, self_le_rpow_of_one_le, self_lt_rpow_of_lt_one, self_lt_rpow_of_one_lt, sqrt_eq_rpow, strictAntiOn_rpow_Ioi_of_exponent_neg, strictAnti_rpow_of_base_lt_one, strictMonoOn_rpow_Ici_of_exponent_pos, strictMono_rpow_of_base_gt_one, zero_rpow, zero_rpow_eq_iff, zero_rpow_le_one, zero_rpow_nonneg, zpow_le_iff_le_log, zpow_le_of_le_log, zpow_lt_iff_lt_log, zpow_lt_of_lt_log	219
Total	225

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_cpow_inv_two_im 📖	mathematical	—	abs Real Real.lattice Real.instAddGroup im Complex instPow instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real.sqrt DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Norm.norm instNorm re Real.instNatCast	—	Nat.instAtLeastTwoHAddOfNat ofReal_ofNat ofReal_inv cpow_ofReal_im div_eq_mul_inv one_div Real.sqrt_eq_rpow abs_mul Real.instIsOrderedRing abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.sqrt_nonneg Real.abs_sin_half Real.sqrt_mul norm_nonneg mul_div_assoc mul_sub mul_one norm_mul_cos_arg
cpow_inv_two_im_eq_neg_sqrt 📖	mathematical	Real Real.instLT im Real.instZero	Complex instPow instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real.instNeg Real.sqrt DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Norm.norm instNorm re Real.instNatCast	—	Nat.instAtLeastTwoHAddOfNat ofReal_ofNat ofReal_inv cpow_ofReal_im div_eq_mul_inv one_div Real.sqrt_eq_rpow Real.sin_half_eq_neg_sqrt le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Real.pi_pos neg_pi_lt_arg LT.lt.le arg_neg_iff mul_neg Real.sqrt_mul norm_nonneg mul_div_assoc mul_sub mul_one norm_mul_cos_arg
cpow_inv_two_im_eq_sqrt 📖	mathematical	Real Real.instLE Real.instZero im	Complex instPow instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real.sqrt DivInvMonoid.toDiv Real.instDivInvMonoid Real.instSub Norm.norm instNorm re Real.instNatCast	—	Nat.instAtLeastTwoHAddOfNat ofReal_ofNat ofReal_inv cpow_ofReal_im div_eq_mul_inv one_div Real.sqrt_eq_rpow Real.sin_half_eq_sqrt arg_nonneg_iff le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Real.pi_pos Mathlib.Tactic.Linarith.sub_nonpos_of_le arg_le_pi Real.sqrt_mul norm_nonneg mul_div_assoc mul_sub mul_one norm_mul_cos_arg
cpow_inv_two_re 📖	mathematical	—	re Complex instPow instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Real.sqrt Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd Norm.norm instNorm Real.instNatCast	—	Nat.instAtLeastTwoHAddOfNat ofReal_ofNat ofReal_inv cpow_ofReal_re div_eq_mul_inv one_div Real.sqrt_eq_rpow Real.cos_half LT.lt.le neg_pi_lt_arg arg_le_pi Real.sqrt_mul norm_nonneg mul_div_assoc mul_add Distrib.leftDistribClass mul_one norm_mul_cos_arg
cpow_mul_ofReal_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Complex instPow ofReal instMul Real.instPow	—	cpow_mul ofReal_log ofReal_mul ofReal_im neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.pi_pos LT.lt.le ofReal_cpow
cpow_ofReal 📖	mathematical	—	Complex instPow ofReal instMul Real Real.instPow Norm.norm instNorm instAdd Real.cos Real.instMul arg Real.sin I	—	eq_or_ne norm_zero ofReal_cpow le_rfl arg_zero MulZeroClass.zero_mul Real.cos_zero Real.sin_zero add_zero mul_one cpow_def_of_ne_zero exp_eq_exp_re_mul_sin_add_cos mul_comm re_ofReal_mul im_ofReal_mul log_re log_im Real.exp_mul Real.exp_log norm_pos_iff
cpow_ofReal_im 📖	mathematical	—	im Complex instPow ofReal Real Real.instMul Real.instPow Norm.norm instNorm Real.sin arg	—	cpow_ofReal ofReal_cos ofReal_sin_ofReal_re cos_ofReal_im mul_one sin_ofReal_im MulZeroClass.mul_zero add_zero zero_add sub_self MulZeroClass.zero_mul
cpow_ofReal_re 📖	mathematical	—	re Complex instPow ofReal Real Real.instMul Real.instPow Norm.norm instNorm Real.cos arg	—	cpow_ofReal ofReal_cos_ofReal_re ofReal_sin MulZeroClass.mul_zero sin_ofReal_im mul_one sub_self add_zero cos_ofReal_im zero_add MulZeroClass.zero_mul sub_zero
inv_natCast_cpow_ofReal_pos 📖	mathematical	—	Complex Preorder.toLT PartialOrder.toPreorder partialOrder instZero instInv instPow instNatCast ofReal	—	RCLike.inv_pos_of_pos ofReal_cpow Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Mathlib.Meta.Positivity.ofReal_pos Real.rpow_pos_of_pos Nat.cast_pos' NeZero.charZero_one RCLike.charZero_rclike lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd
norm_cpow_eq_rpow_re_of_nonneg 📖	mathematical	Real Real.instLE Real.instZero	Norm.norm Complex instNorm instPow ofReal Real.instPow re	—	norm_cpow_of_imp instIsEmptyFalse norm_real abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid arg_ofReal_of_nonneg MulZeroClass.zero_mul Real.exp_zero div_one
norm_cpow_eq_rpow_re_of_pos 📖	mathematical	Real Real.instLT Real.instZero	Norm.norm Complex instNorm instPow ofReal Real.instPow re	—	norm_cpow_of_ne_zero ofReal_ne_zero LT.lt.ne' arg_ofReal_of_nonneg LT.lt.le MulZeroClass.zero_mul Real.exp_zero div_one norm_of_nonneg
norm_cpow_inv_nat 📖	mathematical	—	Norm.norm Complex instNorm instPow instInv instNatCast Real Real.instPow Real.instInv Real.instNatCast	—	norm_cpow_real ofReal_inv
norm_cpow_le 📖	mathematical	—	Real Real.instLE Norm.norm Complex instNorm instPow DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow re Real.exp Real.instMul arg im	—	Eq.le norm_cpow_of_imp zero_cpow norm_zero Real.rpow_zero arg_zero MulZeroClass.zero_mul Real.exp_zero div_self NeZero.charZero_one RCLike.charZero_rclike Real.instZeroLEOneClass
norm_cpow_of_imp 📖	mathematical	Complex instZero	Norm.norm instNorm instPow Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow re Real.exp Real.instMul arg im	—	ne_or_eq norm_cpow_of_ne_zero norm_zero eq_or_ne cpow_zero CStarRing.norm_of_mem_unitary RCLike.instCStarRing instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass Real.rpow_zero arg_zero MulZeroClass.mul_zero Real.exp_zero div_self NeZero.charZero_one RCLike.charZero_rclike Real.zero_rpow zero_div zero_cpow
norm_cpow_of_ne_zero 📖	mathematical	—	Norm.norm Complex instNorm instPow Real DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow re Real.exp Real.instMul arg im	—	cpow_def_of_ne_zero norm_exp mul_re log_re log_im Real.exp_sub Real.rpow_def_of_pos norm_pos_iff
norm_cpow_real 📖	mathematical	—	Norm.norm Complex instNorm instPow ofReal Real Real.instPow	—	norm_cpow_of_imp MulZeroClass.mul_zero Real.exp_zero div_one
norm_log_natCast_le_rpow_div 📖	mathematical	Real Real.instLT Real.instZero	Real.instLE Norm.norm Complex instNorm log instNatCast DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow Real.instNatCast	—	Nat.cast_zero log_zero norm_zero Real.zero_rpow LT.lt.ne' zero_div le_refl natCast_log norm_real Real.norm_of_nonneg Real.log_nonneg Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike GT.gt.lt Real.log_natCast_le_rpow_div
norm_natCast_cpow_le_norm_natCast_cpow_iff 📖	mathematical	—	Real Real.instLE Norm.norm Complex instNorm instPow instNatCast re	—	norm_natCast_cpow_of_pos Real.rpow_le_rpow_left_iff Nat.one_lt_cast IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike
norm_natCast_cpow_le_norm_natCast_cpow_of_pos 📖	mathematical	Real Real.instLE re	Norm.norm Complex instNorm instPow instNatCast	—	norm_natCast_cpow_of_pos Real.rpow_le_rpow_of_exponent_le Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike
norm_natCast_cpow_of_pos 📖	mathematical	—	Norm.norm Complex instNorm instPow instNatCast Real Real.instPow Real.instNatCast re	—	ofReal_natCast norm_cpow_eq_rpow_re_of_pos Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial
norm_natCast_cpow_of_re_ne_zero 📖	mathematical	—	Norm.norm Complex instNorm instPow instNatCast Real Real.instPow Real.instNatCast re	—	ofReal_natCast norm_cpow_eq_rpow_re_of_nonneg Nat.cast_nonneg Real.instIsOrderedRing
norm_natCast_cpow_pos_of_pos 📖	mathematical	—	Real Real.instLT Real.instZero Norm.norm Complex instNorm instPow instNatCast	—	Real.rpow_pos_of_pos Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial norm_natCast_cpow_of_pos
norm_ofReal_cpow_eventually_eq_atTop 📖	mathematical	—	Filter.EventuallyEq Real Filter.atTop Real.instPreorder Norm.norm Complex instNorm instPow ofReal Real.instPow re	—	Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' norm_cpow_eq_rpow_re_of_pos
norm_prime_cpow_le_one_half 📖	mathematical	Real Real.instLT Real.instOne re	Real.instLE Norm.norm Complex instNorm instPow instNatCast Nat.Prime instNeg DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat norm_natCast_cpow_of_re_ne_zero neg_re Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_lt_of_eq neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one neg_eq_zero sub_eq_zero_of_eq Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing LE.le.trans Real.rpow_le_rpow_of_nonpos zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Nat.cast_le Nat.Prime.two_le Subtype.prop le_of_not_gt one_div Real.rpow_neg_one Real.rpow_le_rpow_of_exponent_le one_le_two LT.lt.le neg_lt_neg
ofReal_cpow 📖	mathematical	Real Real.instLE Real.instZero	ofReal Real.instPow Complex instPow	—	Real.rpow_def_of_nonneg ofReal_exp ofReal_mul ofReal_log
ofReal_cpow_of_nonpos 📖	mathematical	Real Real.instLE Real.instZero	Complex instPow ofReal instMul instNeg exp Real.pi I	—	LE.le.eq_or_lt eq_or_ne cpow_zero neg_zero MulZeroClass.mul_zero exp_zero mul_one zero_cpow MulZeroClass.zero_mul ofReal_ne_zero LT.lt.ne cpow_def_of_ne_zero neg_ne_zero exp_add add_mul Distrib.rightDistribClass log.eq_1 norm_neg arg_ofReal_of_neg ofReal_neg arg_ofReal_of_nonneg neg_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ofReal_zero add_zero
one_sub_prime_cpow_ne_zero 📖	—	Nat.Prime Real Real.instLT Real.instOne re	—	—	sub_ne_zero_of_ne Nat.instAtLeastTwoHAddOfNat norm_prime_cpow_le_one_half Mathlib.Meta.NormNum.isRat_le_false Real.instIsStrictOrderedRing IsStrictOrderedRing.toNontrivial Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo NormOneClass.norm_one NormedDivisionRing.to_normOneClass

HasCompactSupport

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rpow_const 📖	mathematical	HasCompactSupport Real Real.instZero	Real.instPow	—	comp_left Real.zero_rpow

Mathlib.Meta.NormNum

Definitions

Name	Category	Theorems
evalRPow 📖	CompOp	—
proveIsNatRPowIsNNRat 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isInt_rpow_neg 📖	mathematical	IsInt Real Real.instRing DivInvMonoid.toZPow Real.instDivInvMonoid	Real.instPow	—	IsInt.out Real.rpow_intCast
isInt_rpow_pos 📖	mathematical	IsNat Real AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing IsInt Monoid.toNatPow Real.instMonoid	Real.instPow	—	IsNat.out Real.rpow_natCast
isNNRat_rpow_neg 📖	mathematical	IsInt Real Real.instRing IsNNRat Real.semiring DivInvMonoid.toZPow Real.instDivInvMonoid	Real.instPow	—	IsInt.out Real.rpow_intCast
isNNRat_rpow_pos 📖	mathematical	IsNat Real AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing IsNNRat Real.semiring Monoid.toNatPow Real.instMonoid	Real.instPow	—	IsNat.out Real.rpow_natCast
isNat_rpow_neg 📖	mathematical	IsInt Real Real.instRing IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivInvMonoid.toZPow Real.instDivInvMonoid	Real.instPow	—	IsInt.out Real.rpow_intCast
isNat_rpow_pos 📖	mathematical	IsNat Real AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing Monoid.toNatPow Real.instMonoid	Real.instPow	—	IsNat.out Real.rpow_natCast
isRat_rpow_neg 📖	mathematical	IsInt Real Real.instRing IsRat DivInvMonoid.toZPow Real.instDivInvMonoid	Real.instPow	—	IsInt.out Real.rpow_intCast
isRat_rpow_pos 📖	mathematical	IsNat Real AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing IsRat Monoid.toNatPow Real.instMonoid	Real.instPow	—	IsNat.out Real.rpow_natCast
rpow_isRat_eq_inv_rpow 📖	mathematical	IsRat Real Real.instRing	Real.instPow Real.instInv DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNatCast	—	Real.rpow_neg_eq_inv_rpow IsRat.neg_to_eq

Mathlib.Meta.NormNum.IsInt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rpow_eq_inv_pow 📖	mathematical	Mathlib.Meta.NormNum.IsInt Real Real.instRing	Real.instPow Real.instInv Monoid.toNatPow Real.instMonoid	—	out Real.rpow_intCast zpow_neg zpow_natCast

Mathlib.Meta.NormNum.IsNNRat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rpow_isNNRat 📖	—	Mathlib.Meta.NormNum.IsNNRat Real Real.semiring Mathlib.Meta.NormNum.IsNat AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing Real.instPow Real.instNatCast	—	—	of_raw Mathlib.Meta.NormNum.IsNat.out LT.lt.ne' Real.rpow_pos_of_pos lt_of_le_of_ne' Nat.cast_nonneg Real.instIsOrderedRing den_nz to_eq Real.div_rpow

Mathlib.Meta.NormNum.IsNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rpow_eq_pow 📖	mathematical	Mathlib.Meta.NormNum.IsNat Real AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing	Real.instPow Monoid.toNatPow Real.instMonoid	—	out Real.rpow_natCast
rpow_isNNRat 📖	mathematical	Mathlib.Meta.NormNum.IsNat Real AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing Mathlib.Meta.NormNum.IsNNRat Real.semiring Monoid.toNatPow Nat.instMonoid	Real.instPow	—	Nat.cast_zero RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsNNRat.to_eq div_eq_mul_inv Real.rpow_natCast_mul Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass Nat.cast_pow Real.pow_rpow_inv_natCast ne_of_gt lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalRpow 📖	CompOp	—
evalRpowZero 📖	CompOp	—

Real

Definitions

Name	Category	Theorems
instPow 📖	CompOp	666 math math: ENNReal.ofReal_rpow_of_pos, CuspFormClass.qExpansion_isBigO, rpow_eq_pow, NumberField.mixedEmbedding.fundamentalCone.expMapBasis_apply', PiLp.norm_toLp_const', rpow_add_of_nonneg, ContinuousOn.rpow, ContinuousWithinAt.rpow_const, HasDerivAt.const_rpow, hasMeasurablePow, Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le, MeasureTheory.norm_indicatorConstLp_le, ProbabilityTheory.gammaPDF_of_nonneg, logb_le_iff_le_rpow, HasStrictDerivAt.rpow, ContDiffOn.rpow_const_of_le, rpow_lt_one_iff_of_pos, ProbabilityTheory.betaPDF_eq, rpow_add_natCast', AkraBazziRecurrence.tendsto_zero_sumCoeffsExp, rpow_eq_nhds_of_neg, Complex.isTheta_cpow_rpow, isLittleO_exp_neg_mul_sq_cocompact, young_inequality, CFC.tendsto_cfc_rpow_sub_one_log, one_le_rpow_of_pos_of_le_one_of_nonpos, rpow_le_self_of_one_le, hasStrictDerivAt_rpow_const_of_ne, monotone_rpow_of_base_ge_one, Asymptotics.IsLittleO.rpow, strictConcaveOn_rpow, PiLp.norm_toLp_one, rpow_pos_of_pos, exp_mul, inv_rpow, Metric.Snowflaking.preimage_ofSnowflaking_closedBall, MeasureTheory.integral_mul_norm_le_Lp_mul_Lq, tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero, EisensteinSeries.summand_bound_of_mem_verticalStrip, lt_rpow_inv_iff_of_pos, MeasureTheory.norm_indicatorConstLp, continuous_rpow_const, AkraBazziRecurrence.tendsto_atTop_sumCoeffsExp, ContDiffPointwiseHolderAt.isBigO, rpow_neg_one, rpow_zpow_comm, Complex.cpow_mul_ofReal_nonneg, rpow_eq_const_mul_integral, ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet, summable_one_div_nat_add_rpow, logb_le_iff_le_rpow_of_base_lt_one, isLittleO_log_rpow_rpow_atTop, Differentiable.fderiv_norm_rpow, MeasureTheory.MemLp.integrable_norm_rpow', rpow_def_of_pos, AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_sub_smoothingFn, MeasureTheory.MemLp.norm_rpow, lp.sum_rpow_le_norm_rpow, setOf_liouvilleWith_subset_aux, lp.norm_sum_single, contDiffAt_rpow_const_of_le, hasStrictFDerivAt_rpow_of_pos, rpow_sum_le_const_mul_sum_rpow_of_nonneg, WeakFEPair.hf_zero', integral_exp_neg_mul_rpow, Mathlib.Meta.NormNum.rpow_isRat_eq_inv_rpow, summable_nat_rpow_inv, integrableOn_Ioi_rpow_of_lt, list_prod_map_rpow', ContinuousMap.toLp_norm_le, WeakFEPair.h_feq, Complex.integral_rpow_mul_exp_neg_rpow, integral_Ioi_rpow_of_lt, Complex.volume_sum_rpow_le, ContDiffOn.rpow, rpow_inv_log, enorm_fderiv_norm_rpow_le, lp.sum_rpow_le_of_tendsto, le_logb_iff_rpow_le, rpow_mul_intCast, setIntegral_Ioi_zero_rpow, integral_rpow_mul_exp_neg_rpow, logb_lt_iff_lt_rpow, GammaIntegral_convergent, MeasureTheory.measure_lt_one_eq_integral_div_gamma, one_add_rpow_hasFPowerSeriesOnBall_zero, Mathlib.Meta.NormNum.isRat_rpow_pos, Chebyshev.psi_eq_sum_theta, MeasureTheory.integrable_norm_rpow_iff, MeasureTheory.MemLp.exists_boundedContinuous_integral_rpow_sub_le, self_le_rpow_of_le_one, logb_eq_iff_rpow_eq, WithLp.prod_norm_eq_of_nat, rpowIntegrand₀₁_le_rpow_sub_two_mul_self, lp.norm_rpow_eq_tsum, integrable_one_add_norm, Gamma_mul_Gamma_add_half, integrableOn_add_rpow_Ioi_of_lt, NNReal.coe_rpow, harm_mean_le_geom_mean_weighted, DifferentiableOn.rpow, ZLattice.tsum_norm_rpow_le, DifferentiableAt.rpow_const, differentiableAt_rpow_const_of_ne, summable_abs_int_rpow, multiset_prod_map_rpow, ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet, PeriodPair.weierstrassP_bound, deriv_norm_ofReal_cpow, Complex.ofReal_cpow, tendsto_rpow_atTop, deriv_rpow_const, convexOn_rpow_left, tendsto_smoothingFun_comp, AkraBazziRecurrence.sumTransform_def, rpow_lt_rpow_of_neg, Mathlib.Meta.NormNum.isNNRat_rpow_pos, continuousAt_rpow_const, log_rpow, tsum_exp_neg_mul_int_sq, Asymptotics.IsBigOWith.rpow, rpow_mul_natCast, rpow_sub', LSeries.summable_real_of_abscissaOfAbsConv_lt, Continuous.rpow, finite_integral_rpow_sub_one_pow_aux, Complex.GammaIntegral_ofReal, Complex.norm_cpow_of_ne_zero, memℓp_gen_iff, Complex.norm_ofReal_cpow_eventually_eq_atTop, differentiableOn_rpow_const, Complex.integral_exp_neg_rpow, harm_mean_le_geom_mean, continuousAt_rpow_of_pos, MeasureTheory.integral_comp_rpow_Ioi_of_pos, rpow_eq_zero_iff_of_nonneg, ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet, continuousAt_const_rpow', ZLattice.tsumNormRPowBound_spec, ContDiffOn.rpow_const_of_ne, Complex.norm_cpow_of_imp, rpow_lt_rpow_left_iff, HasDerivWithinAt.const_rpow, hasFDerivAt_norm_rpow, MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul, intervalIntegral.integrableOn_Ioo_rpow_iff, concaveOn_rpow, mul_rpow, rpow_le_rpow_of_nonpos, MeasureTheory.volume_sum_rpow_lt, hasDerivAt_abs_rpow, logb_rpow_eq_mul_logb_of_pos, ZetaAsymptotics.term_tsum_of_lt, Rat.AbsoluteValue.exists_nat_rpow_iff_isEquiv, rpow_arith_mean_le_arith_mean_rpow, Rat.AbsoluteValue.equiv_on_nat_iff_equiv, ContDiff.norm_rpow, MeasureTheory.Measure.HasTemperateGrowth.exists_integrable, ENNReal.ofReal_rpow_of_nonneg, integrable_rpow_neg_one_add_norm_sq, rpow_zero, Complex.cpow_ofReal_re, le_rpow_add, Chebyshev.sum_PrimePow_eq_sum_sum, StrongFEPair.hf_zero', differentiableAt_rpow_of_ne, Metric.Snowflaking.image_ofSnowflaking_ball, rpow_lt_rpow_of_exponent_neg, ProbabilityTheory.integrable_rpow_abs_mul_exp_of_integrable_exp_mul, le_rpow_inv_iff_of_neg, log_le_rpow_div, LSeriesSummable.le_const_mul_rpow, intervalIntegral.intervalIntegrable_rpow, AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_sub_smoothingFn, ContDiffAt.rpow, Complex.norm_cpow_real, tendsto_rpow_atTop_of_base_gt_one, Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma, isLittleO_exp_mul_rpow_of_lt, rpow_eq_zero, Complex.isBigO_cpow_rpow, rpowIntegrand₀₁_apply_mul_eqOn_Ici, ProbabilityTheory.betaPDF_of_pos_lt_one, Complex.HadamardThreeLines.norm_invInterpStrip, MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul, exp_one_rpow, WithLp.prod_norm_eq_add, strictAntiOn_rpow_Ioi_of_exponent_neg, MeasureTheory.Lp.norm_const_le, MeasureTheory.volume_sum_rpow_le, geom_mean_eq_arith_mean_weighted_iff', integral_rpow_mul_exp_neg_mul_rpow, ProbabilityTheory.paretoPDF_of_le, HasStrictFDerivAt.rpow, rpow_def_of_neg, le_rpow_one_add_norm_iff_norm_le, Matrix.frobenius_norm_def, RingSeminorm.exists_index_pow_le, Behrend.bound, PiLp.norm_eq_sum, inner_le_weight_mul_Lp_of_nonneg, WeakFEPair.h_feq', rpow_sum_le_const_mul_sum_rpow, AkraBazziRecurrence.asympBound_def, Mathlib.Meta.NormNum.isNat_rpow_neg, tendsto_rpow_div_mul_add, rpow_sum_of_pos, tendsto_rpow_atTop_of_base_lt_one, NumberField.house.exists_ne_zero_int_vec_house_le, WithLp.prod_norm_eq_add_idemFst, norm_inv_mul_rpow_sub_one_sub_log_le, Metric.Snowflaking.preimage_toSnowflaking_closedBall, strictMono_rpow_of_base_gt_one, isLittleO_rpow_exp_pos_mul_atTop, one_rpow, AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_add_smoothingFn, contDiffPointwiseHolderAt_iff, Mathlib.Meta.NormNum.IsNat.rpow_isNNRat, HasDerivWithinAt.rpow, MeasureTheory.Lp.norm_const', AkraBazziRecurrence.p_def, ContDiffAt.rpow_const_of_ne, monotoneOn_rpow_Ici_of_exponent_nonneg, RingSeminorm.isBoundedUnder, not_integrableOn_Ioi_rpow, tendsto_rpow_sub_one_log, ZLattice.summable_norm_rpow, arith_mean_le_rpow_mean, NumberField.mixedEmbedding.fundamentalCone.expMap_smul, continuous_const_rpow, rpow_logb_eq_abs, Filter.Tendsto.rpow_const, one_lt_rpow_iff_of_pos, hasStrictDerivAt_const_rpow_of_neg, AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_add_smoothingFn, MeasureTheory.MemLp.integrable_norm_rpow, isLittleO_log_rpow_nhdsGT_zero, abs_rpow_of_nonneg, Mathlib.Meta.NormNum.isRat_rpow_neg, AkraBazziRecurrence.strictAnti_sumCoeffsExp, isLittleO_log_rpow_atTop, le_rpow_iff_log_le, div_rpow, isLittleO_exp_neg_mul_rpow_atTop, tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact, rpow_lt_one, derivWithin_const_rpow, norm_fderiv_norm_rpow_le, smoothingFun_le, deriv_rpow_const, geom_mean_le_arith_mean4_weighted, ContDiff.rpow, zero_rpow_eq_iff, Differentiable.norm_rpow, eq_zero_rpow_iff, logb_lt_iff_lt_rpow_of_base_lt_one, LSeries.norm_term_eq, antitone_rpow_of_base_le_one, MeasureTheory.lpNorm_nnreal_eq_integral_norm_rpow, derivWithin_rpow_const, Complex.integral_exp_neg_mul_rpow, le_rpow_inv_iff_of_pos, pow_rpow_inv_natCast, MeasureTheory.MemLp.eLpNorm_eq_integral_rpow_norm, rpow_one_add', rpow_le_rpow_of_exponent_ge', abs_rpow_le_abs_rpow, HurwitzZeta.oddKernel_functional_equation, MeasureTheory.MemLp.exists_hasCompactSupport_integral_rpow_sub_le, finite_integral_one_add_norm, WeakFEPair.hg_top, isLittleO_abs_log_rpow_rpow_nhdsGT_zero, ContinuousAt.rpow, EisensteinSeries.summable_one_div_norm_rpow, rpow_le_rpow_left_iff, hasDerivAt_rpow_const, rpow_logb, rpow_lt_rpow_iff_of_neg, zero_rpow, rpowIntegrand₀₁_apply_mul, rpow_one, BoundedContinuousFunction.Lp_norm_le, MeasureTheory.Lp.norm_constL_le, isTheta_deriv_rpow_const_atTop, rpow_left_inj, Complex.volume_sum_rpow_lt, lp.norm_compl_sum_single, MeasureTheory.integral_comp_rpow_Ioi, integrable_rpow_mul_exp_neg_mul_sq, SchwartzMap.integral_pow_mul_iteratedFDeriv_le, integral_exp_neg_rpow, WeakFEPair.hf_zero, HasCompactSupport.rpow_const, rpow_neg_eq_inv_rpow, rpow_add_one, lt_rpow_inv_iff_of_neg, WithLp.prod_dist_eq_add, one_div_one_sub_rpow_hasFPowerSeriesOnBall_zero, add_rpow_le_rpow_add, continuousAt_rpow_of_ne, MeasureTheory.Lp.norm_const, lt_logb_iff_rpow_lt, tendsto_log_div_rpow_nhdsGT_zero, geom_mean_le_arith_mean3_weighted, ZetaAsymptotics.zeta_limit_aux1, rpow_intCast_mul, ContDiffWithinAt.rpow, list_prod_map_rpow, rpow_inv_le_iff_of_neg, Chebyshev.psi_eq_theta_add_sum_theta, rpow_lt_one_of_one_lt_of_neg, rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg, summable_one_div_nat_rpow, rpow_sub_one, LiouvilleWith.frequently_lt_rpow_neg, AkraBazziRecurrence.asympBound_def', ProbabilityTheory.integrable_rpow_abs_mul_exp_add_of_integrable_exp_mul, Tactic.ComputeAsymptotics.Majorized.self, HasDerivAt.rpow, Complex.norm_natCast_cpow_of_pos, isLittleO_rpow_exp_atTop, tendsto_rpow_neg_nhdsGT_zero, Filter.Tendsto.rpow, HasFDerivWithinAt.rpow_const, one_le_rpow, cexp_neg_quadratic_isLittleO_abs_rpow_cocompact, Rat.AbsoluteValue.exists_pos_eq_pow_neg, integrableOn_Ioi_rpow_iff, ZetaAsymptotics.term_sum_of_lt, deriv_const_rpow, ContDiffAt.rpow_const_of_le, MeasureTheory.Lp.norm_le_of_ae_bound, rpowIntegrand₀₁_eq_pow_div, contDiffAt_rpow_const, Metric.Snowflaking.preimage_ofSnowflaking_ball, integrableOn_rpow_mul_exp_neg_rpow, rpow_sub_one', ContDiff.rpow_const_of_le, rpow_lt_rpow, rpow_two, ProbabilityTheory.paretoPDF_eq, DifferentiableAt.rpow, rpow_logb_of_neg, Lp_add_le, integral_rpow, Lp_add_le_of_nonneg, rpow_add', Mathlib.Meta.NormNum.IsInt.rpow_eq_inv_pow, MeasureTheory.MemLp.norm_rpow_div, strictConvexOn_rpow, rpow_le_rpow_left_iff_of_base_lt_one, rpow_inv_log_le_exp_one, ContDiff.rpow_const_of_ne, HasFDerivAt.rpow_const, geom_mean_lt_arith_mean_weighted_iff_of_pos, HasStrictFDerivAt.const_rpow, pow_mul_le_of_le_of_pow_mul_le, CuspFormClass.exists_bound, Gamma_eq_integral, ProbabilityTheory.integrable_rpow_abs_of_integrable_exp_mul, abs_log_mul_self_rpow_lt, rpow_left_injOn, mellin_comp_rpow, rpow_sub_intCast', MeasureTheory.memLp_norm_rpow_iff, rpow_sum_of_nonneg, Mathlib.Meta.NormNum.isNNRat_rpow_neg, tendstoLocallyUniformlyOn_rpow_sub_one_log, lp.hasSum_norm, self_lt_rpow_of_lt_one, MeasureTheory.eLpNorm_norm_rpow, rpow_le_self_of_le_one, tendsto_rpow_atBot_of_base_lt_one, one_lt_rpow_of_pos_of_lt_one_of_neg, LiouvilleWith.exists_pos, rpow_add_rpow_le_add, PiLp.norm_eq_of_nat, MellinConvergent.comp_rpow, PiLp.norm_toLp_const, ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul, nnnorm_fderiv_norm_rpow_le, ProbabilityTheory.integrable_rpow_abs_of_mem_interior_integrableExpSet, Complex.isTheta_cpow_const_rpow, Metric.Snowflaking.preimage_toSnowflaking_ball, rpow_inv_natCast_pow, Gamma_mul_Gamma_add_half_of_pos, rpow_def_of_nonneg, ZLattice.summable_norm_sub_rpow, one_add_rpow_hasFPowerSeriesAt_zero, MeasureTheory.lpNorm_one, ArithmeticFunction.vonMangoldt.LSeries_residueClass_lower_bound, spectralNorm.spectralNorm_eq_norm_coeff_zero_rpow, ContinuousAt.rpow_const, not_differentiableAt_rpow_const_zero, rpow_le_iff_le_log, exp_neg_mul_rpow_isLittleO_exp_neg, mellin_convergent_iff_norm, DifferentiableWithinAt.rpow_const, tendsto_rpow_div, HasFDerivWithinAt.rpow, AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn, geom_mean_eq_arith_mean_weighted_iff, one_add_rpow_hasFPowerSeriesAt_zero, rpow_sub_natCast', geom_mean_le_arith_mean, lp.norm_sub_norm_compl_sub_single, rpow_le_of_le_log, rpow_le_one, rpow_lt_one_iff, Asymptotics.IsBigO.rpow_rpow_nhdsGE_zero_of_le_of_imp, WeakFEPair.hf_modif_FE, rpow_add_rpow_le, HasDerivWithinAt.rpow_const, ProbabilityTheory.gammaPDF_eq, spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius, isBigO_deriv_ofReal_cpow_const_atTop, ContDiffWithinAt.rpow_const_of_ne, hasDerivAt_norm_rpow, ProbabilityTheory.rpow_abs_le_mul_max_exp, tendsto_rpow_neg_div, zero_mem_lowerBounds_smoothingSeminormSeq_range, tendsto_rpow_neg_atTop, rexp_neg_quadratic_isLittleO_rpow_atTop, HasFDerivAt.const_rpow, rpow_inv_lt_iff_of_neg, ContDiffWithinAt.rpow_const_of_le, continuousAt_const_rpow, Asymptotics.IsTheta.rpow, enorm_rpow_of_nonneg, LSeriesSummable.isBigO_rpow, cexp_neg_quadratic_isLittleO_rpow_atTop, smoothingSeminormSeq_bddBelow, Complex.cpow_ofReal_im, tendsto_sub_mul_tsum_nat_rpow, contDiff_rpow_const_of_le, rpow_lt_iff_lt_log, ProbabilityTheory.lintegral_betaPDF, rpow_le_rpow, BoundedContinuousFunction.toLp_norm_le, Metric.Snowflaking.image_toSnowflaking_closedBall, mul_log_eq_log_iff, ProbabilityTheory.rpow_abs_le_mul_exp_abs, strictAnti_rpow_of_base_lt_one, tendsto_one_add_rpow_exp_of_tendsto, rpow_neg_one_add_norm_sq_le, contDiffAt_rpow_const_of_ne, rpow_ofNat, Mathlib.Meta.NormNum.isInt_rpow_pos, rpow_add, Nat.Primes.summable_rpow, isBigO_deriv_rpow_const_atTop, deriv_rpow_const', MeasureTheory.integral_mul_le_Lp_mul_Lq_of_nonneg, HasDerivAt.rpow_const, DifferentiableOn.rpow_const, inner_le_Lp_mul_Lq, iter_deriv_rpow_const, rpow_add_le_add_rpow, Complex.norm_cpow_inv_nat, rpow_one_sub', ProbabilityTheory.rpow_abs_le_mul_max_exp_of_pos, Complex.integral_rpow_mul_exp_neg_mul_rpow, rpow_sub_natCast, rpow_inv_eq, MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top, integral_pow_mul_le_of_le_of_pow_mul_le, CFC.nnrpow_eq_cfcₙ_real, rpow_eq_nhds_of_pos, ENNReal.toReal_rpow, Asymptotics.IsBigO.rpow, continuousAt_rpow, rpow_one_add_lt_one_add_mul_self, closedBall_rpow_sub_one_eq_empty_aux, StrongFEPair.hf_top', rpow_le_rpow_of_exponent_nonpos, integral_rpow_mul_exp_neg_mul_Ioi, rpow_le_one_of_one_le_of_nonpos, rpow_le_rpow_iff, rpow_max, differentiable_norm_rpow, rpow_add_natCast, log_natCast_le_rpow_div, Memℓp.summable, tendsto_exp_div_rpow_atTop, Gamma_integrand_isLittleO, rpow_nonneg, Complex.norm_cpow_eq_rpow_re_of_nonneg, NumberField.abs_discr_rpow_ge_of_isTotallyComplex, CFC.norm_rpow, self_lt_rpow_of_one_lt, rpow_pow_comm, intervalIntegral.intervalIntegrable_rpow', HolderOnWith.dist_le, HasFDerivWithinAt.const_rpow, ZetaAsymptotics.term_welldef, geom_mean_eq_arith_mean_weighted_of_constant, rpow_div_two_eq_sqrt, young_inequality_of_nonneg, antitoneOn_rpow_Ioi_of_exponent_nonpos, Metric.Snowflaking.dist_ofSnowflaking_ofSnowflaking, lp.norm_eq_tsum_rpow, WeakFEPair.f_modif_aux1, geom_mean_weighted_of_constant, Asymptotics.IsBigO.id_rpow_of_le_one, HolderWith.dist_le_of_le, Metric.Snowflaking.image_ofSnowflaking_closedBall, HurwitzZeta.evenKernel_functional_equation, Complex.norm_log_natCast_le_rpow_div, Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip', integrableOn_rpow_mul_exp_neg_mul_sq, AbsoluteValue.isEquiv_iff_exists_rpow_eq, CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one, nnnorm_rpow_of_nonneg, AkraBazziRecurrence.growsPolynomially_rpow, Bertrand.real_main_inequality, MeasureTheory.lpNorm_eq_integral_norm_rpow_toReal, rpow_lt_self_of_one_lt, Complex.volume_sum_rpow_lt_one, rpow_le_rpow_iff_of_neg, rpow_def_of_nonpos, rpow_le_rpow_of_exponent_ge, ContinuousOn.rpow_const, Mathlib.Meta.NormNum.IsNat.rpow_eq_pow, MeasureTheory.norm_indicatorConstLp', AkraBazziRecurrence.one_mem_range_sumCoeffsExp, AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn, rpow_sub_intCast, Continuous.rpow_const, rpow_le_one_iff_of_pos, norm_rpow_of_nonneg, abs_rpow_le_exp_log_mul, rpow_sub, rpow_le_rpow_of_exponent_ge_of_imp, contDiff_norm_rpow, rpow_inv_lt_iff_of_pos, HolderWith.dist_le, fderiv_norm_rpow, MeasureTheory.lpNorm_one', isTheta_deriv_ofReal_cpow_const_atTop, hasStrictDerivAt_const_rpow, ProbabilityTheory.integrable_rpow_of_integrable_exp_mul, rpowIntegrand₀₁_le_rpow_sub_one, rpow_lt_rpow_iff, rpow_mul, AkraBazziRecurrence.continuous_sumCoeffsExp, integral_mul_rpow_one_add_sq, rpow_of_add_eq, differentiable_rpow_const, rpow_add_intCast, lt_logb_iff_rpow_lt_of_base_lt_one, Complex.norm_cpow_le, MeasureTheory.lpNorm_const, rpow_rpow_inv, ProbabilityTheory.integrable_rpow_of_mem_interior_integrableExpSet, one_add_mul_self_lt_rpow_one_add, rpow_lt_rpow_of_exponent_gt, compact_inner_le_weight_mul_Lp_of_nonneg, toNNReal_rpow_of_nonneg, Differentiable.rpow_const, le_logb_iff_rpow_le_of_base_lt_one, hasStrictFDerivAt_rpow_of_neg, hasStrictDerivAt_rpow_const, integral_rpowIntegrand₀₁_eq_rpow_mul_const, lt_rpow_of_log_lt, rpow_neg_natCast, Metric.Snowflaking.image_toSnowflaking_ball, one_lt_rpow, rpowIntegrand₀₁_apply_mul', Asymptotics.IsEquivalent.rpow, strictMonoOn_rpow_Ici_of_exponent_pos, MeasureTheory.integrableOn_Ioi_comp_rpow_iff, rpow_right_inj, spectralValueTerms_of_lt_natDegree, finset_prod_rpow, ZLattice.sum_piFinset_Icc_rpow_le, tendsto_log_mul_rpow_nhdsGT_zero, rpow_inv_le_iff_of_pos, AkraBazziRecurrence.injective_sumCoeffsExp, pi_rpow_zero, MeasureTheory.eLpNorm'_norm_rpow, ContinuousWithinAt.rpow, MeasureTheory.measure_unitBall_eq_integral_div_gamma, ZetaAsymptotics.term_of_lt, AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn, Complex.norm_cpow_eq_rpow_re_of_pos, log_div_self_rpow_antitoneOn, rpow_inv_rpow, rpow_neg, Function.hasTemperateGrowth_one_add_norm_sq_rpow, rpow_add_intCast', AkraBazziRecurrence.sumCoeffsExp_p_eq_one, rpow_intCast, rpow_one_add_le_one_add_mul_self, DifferentiableWithinAt.rpow, self_le_rpow_of_one_le, Differentiable.rpow, logb_rpow, norm_fderiv_norm_id_rpow, rpow_le_rpow_of_exponent_le_or_ge, rpowIntegrand₀₁_one_ge_rpow_sub_two, ContDiffPointwiseHolderAt.zero_order_iff, MeasureTheory.lpNorm_const', tendsto_one_add_div_rpow_exp, rpow_add_one', rpow_lt_self_of_lt_one, exists_measure_rpow_eq_integral, Mathlib.Meta.NormNum.isNat_rpow_pos, EisensteinSeries.summand_bound, Complex.HadamardThreeLines.norm_le_interp_of_mem_verticalClosedStrip₀₁', tendsto_exp_mul_div_rpow_atTop, sqrt_eq_rpow, contDiffAt_rpow_of_ne, Metric.Snowflaking.dist_toSnowflaking_toSnowflaking, CFC.norm_nnrpow, one_add_rpow_hasFPowerSeriesOnBall_zero, rpow_def, summable_nat_rpow, one_add_mul_self_le_rpow_one_add, MeasureTheory.L2.eLpNorm_rpow_two_norm_lt_top, rpowIntegrand₀₁_eqOn_mul_rpowIntegrand₀₁_one, HasFDerivAt.rpow, rpow_natCast, zero_rpow_nonneg, inner_le_Lp_mul_Lq_of_nonneg, MeasureTheory.volume_sum_rpow_lt_one, Mathlib.Meta.NormNum.isInt_rpow_neg, rpow_natCast_mul, lt_rpow_iff_log_lt, convexOn_rpow, summable_one_div_int_add_rpow, rpow_zero_pos, Complex.norm_natCast_cpow_of_re_ne_zero, Int.Matrix.exists_ne_zero_int_vec_norm_le, AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn, WeakFEPair.hf_top, PiLp.dist_eq_sum, AkraBazziRecurrence.GrowsPolynomially.rpow, SchwartzMap.isBigO_cocompact_rpow, le_rpow_of_log_le, MeasureTheory.integrableOn_Ioi_comp_rpow_iff', geom_mean_le_arith_mean2_weighted, integrableAtFilter_rpow_atTop_iff, CFC.rpow_eq_cfc_real, rpow_le_rpow_of_exponent_le, rpowIntegrand₀₁_eqOn_pow_div, rpow_neg_ofNat, Complex.cpow_ofReal, rpow_lt_of_lt_log, one_lt_rpow_iff, HolderOnWith.dist_le_of_le, ZLattice.exists_finsetSum_norm_rpow_le_tsum, MeasureTheory.Measure.integrable_pow_neg_integrablePower, zero_rpow_le_one, GaussianFourier.integral_rexp_neg_mul_sq_norm, integrableOn_rpow_mul_exp_neg_mul_rpow, rpow_lt_rpow_left_iff_of_base_lt_one, Int.Matrix.exists_ne_zero_int_vec_norm_le', HasStrictFDerivAt.rpow_const, eq_rpow_inv, tendsto_rpow_atBot_of_base_gt_one, Rat.AbsoluteValue.le_pow_log, rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg, geom_mean_le_arith_mean_weighted, rpow_lt_one_iff', rpow_lt_rpow_of_exponent_lt, ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet
rpow 📖	CompOp	1 math math: rpow_eq_pow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_log_mul_self_rpow_lt 📖	mathematical	Real instLT instZero instLE instOne	abs lattice instAddGroup instMul log instPow DivInvMonoid.toDiv instDivInvMonoid	—	lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing abs_log_mul_self_lt rpow_pos_of_pos rpow_le_one LT.lt.le mul_comm abs_of_pos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid abs_mul instIsOrderedRing mul_assoc log_rpow
abs_rpow_le_abs_rpow 📖	mathematical	—	Real instLE abs lattice instAddGroup instPow	—	le_or_gt abs_rpow_of_nonneg le_refl abs_of_neg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid rpow_def_of_neg rpow_def_of_pos neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd log_neg_eq_log abs_mul instIsOrderedRing abs_of_pos exp_pos mul_le_of_le_one_right IsOrderedRing.toPosMulMono LT.lt.le abs_cos_le_one
abs_rpow_le_exp_log_mul 📖	mathematical	—	Real instLE abs lattice instAddGroup instPow exp instMul log	—	LE.le.trans abs_rpow_le_abs_rpow abs_zero IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid rpow_zero log_zero MulZeroClass.mul_zero exp_zero zero_rpow MulZeroClass.zero_mul instZeroLEOneClass rpow_def_of_pos abs_pos log_abs le_refl
abs_rpow_of_nonneg 📖	mathematical	Real instLE instZero	abs lattice instAddGroup instPow	—	rpow_nonneg abs_eq_self instIsOrderedAddMonoid
antitoneOn_rpow_Ioi_of_exponent_nonpos 📖	mathematical	Real instLE instZero	AntitoneOn instPreorder instPow Set.Ioi	—	rpow_le_rpow_of_nonpos
antitone_rpow_of_base_le_one 📖	mathematical	Real instLT instZero instLE instOne	Antitone instPreorder instPow	—	lt_or_eq_of_le StrictAnti.antitone strictAnti_rpow_of_base_lt_one one_rpow
div_rpow 📖	mathematical	Real instLE instZero	instPow DivInvMonoid.toDiv instDivInvMonoid	—	div_eq_mul_inv mul_rpow inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing inv_rpow
eq_rpow_inv 📖	mathematical	Real instLE instZero	instPow instInv	—	rpow_nonneg rpow_inv_rpow
eq_zero_rpow_iff 📖	mathematical	—	Real instPow instZero instOne	—	zero_rpow_eq_iff
exp_mul 📖	mathematical	—	exp Real instMul instPow	—	rpow_def_of_pos exp_pos log_exp
exp_one_pow 📖	mathematical	—	Real Monoid.toNatPow instMonoid exp instOne instNatCast	—	rpow_natCast exp_one_rpow
exp_one_rpow 📖	mathematical	—	Real instPow exp instOne	—	exp_mul one_mul
inv_rpow 📖	mathematical	Real instLE instZero	instPow instInv	—	rpow_neg_eq_inv_rpow rpow_neg
le_log_of_pow_le 📖	mathematical	Real instLT instZero instLE Monoid.toNatPow instMonoid	instMul instNatCast log	—	le_log_of_rpow_le rpow_natCast
le_log_of_rpow_le 📖	mathematical	Real instLT instZero instLE instPow	instMul log	—	log_le_log rpow_pos_of_pos log_rpow
le_log_of_zpow_le 📖	mathematical	Real instLT instZero instLE DivInvMonoid.toZPow instDivInvMonoid	instMul instIntCast log	—	le_log_of_rpow_le rpow_intCast
le_pow_iff_log_le 📖	mathematical	Real instLT instZero	instLE Monoid.toNatPow instMonoid log instMul instNatCast	—	le_rpow_iff_log_le rpow_natCast
le_pow_of_log_le 📖	mathematical	Real instLT instZero instLE log instMul instNatCast	Monoid.toNatPow instMonoid	—	le_rpow_of_log_le rpow_natCast
le_rpow_add 📖	mathematical	Real instLE instZero	instMul instPow instAdd	—	le_iff_eq_or_lt rpow_zero mul_le_mul IsOrderedRing.toPosMulMono instIsOrderedRing IsOrderedRing.toMulPosMono zero_rpow_le_one zero_rpow_nonneg zero_le_one instZeroLEOneClass mul_one rpow_add' rpow_add
le_rpow_iff_log_le 📖	mathematical	Real instLT instZero	instLE instPow log instMul	—	log_le_log_iff rpow_pos_of_pos log_rpow
le_rpow_inv_iff_of_neg 📖	mathematical	Real instLT instZero	instLE instPow instInv	—	rpow_le_rpow_iff_of_neg rpow_pos_of_pos rpow_inv_rpow le_of_lt LT.lt.ne
le_rpow_inv_iff_of_pos 📖	mathematical	Real instLE instZero instLT	instPow instInv	—	rpow_le_rpow_iff rpow_nonneg rpow_inv_rpow ne_of_gt
le_rpow_of_log_le 📖	mathematical	Real instLT instZero instLE log instMul	instPow	—	le_or_gt LE.le.trans LT.lt.le rpow_pos_of_pos le_rpow_iff_log_le
le_zpow_iff_log_le 📖	mathematical	Real instLT instZero	instLE DivInvMonoid.toZPow instDivInvMonoid log instMul instIntCast	—	le_rpow_iff_log_le rpow_intCast
le_zpow_of_log_le 📖	mathematical	Real instLT instZero instLE log instMul instIntCast	DivInvMonoid.toZPow instDivInvMonoid	—	le_rpow_of_log_le rpow_intCast
log_le_rpow_div 📖	mathematical	Real instLE instZero instLT	log DivInvMonoid.toDiv instDivInvMonoid instPow	—	LE.le.eq_or_lt log_zero zero_rpow LT.lt.ne' zero_div le_refl le_div_iff₀' PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing Eq.trans_le log_rpow LE.le.trans log_le_sub_one_of_pos rpow_pos_of_pos LT.lt.le sub_one_lt instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
log_natCast_le_rpow_div 📖	mathematical	Real instLT instZero	instLE log instNatCast DivInvMonoid.toDiv instDivInvMonoid instPow	—	log_le_rpow_div Nat.cast_nonneg instIsOrderedRing
log_rpow 📖	mathematical	Real instLT instZero	log instPow instMul	—	exp_injective exp_log rpow_pos_of_pos mul_comm rpow_def_of_pos exp_pos
lt_log_of_pow_lt 📖	mathematical	Real instLT instZero Monoid.toNatPow instMonoid	instMul instNatCast log	—	lt_log_of_rpow_lt rpow_natCast
lt_log_of_rpow_lt 📖	mathematical	Real instLT instZero instPow	instMul log	—	log_lt_log rpow_pos_of_pos log_rpow
lt_log_of_zpow_lt 📖	mathematical	Real instLT instZero DivInvMonoid.toZPow instDivInvMonoid	instMul instIntCast log	—	lt_log_of_rpow_lt rpow_intCast
lt_pow_iff_log_lt 📖	mathematical	Real instLT instZero	Monoid.toNatPow instMonoid log instMul instNatCast	—	lt_rpow_iff_log_lt rpow_natCast
lt_pow_of_log_lt 📖	mathematical	Real instLT instZero log instMul instNatCast	Monoid.toNatPow instMonoid	—	lt_rpow_of_log_lt rpow_natCast
lt_rpow_iff_log_lt 📖	mathematical	Real instLT instZero	instPow log instMul	—	log_lt_log_iff rpow_pos_of_pos log_rpow
lt_rpow_inv_iff_of_neg 📖	mathematical	Real instLT instZero	instPow instInv	—	rpow_lt_rpow_iff_of_neg rpow_pos_of_pos rpow_inv_rpow le_of_lt LT.lt.ne
lt_rpow_inv_iff_of_pos 📖	mathematical	Real instLE instZero instLT	instPow instInv	—	lt_iff_lt_of_le_iff_le rpow_inv_le_iff_of_pos
lt_rpow_of_log_lt 📖	mathematical	Real instLT instZero log instMul	instPow	—	le_or_gt LE.le.trans_lt rpow_pos_of_pos lt_rpow_iff_log_lt
lt_zpow_iff_log_lt 📖	mathematical	Real instLT instZero	DivInvMonoid.toZPow instDivInvMonoid log instMul instIntCast	—	lt_rpow_iff_log_lt rpow_intCast
lt_zpow_of_log_lt 📖	mathematical	Real instLT instZero log instMul instIntCast	DivInvMonoid.toZPow instDivInvMonoid	—	lt_rpow_of_log_lt rpow_intCast
monotoneOn_rpow_Ici_of_exponent_nonneg 📖	mathematical	Real instLE instZero	MonotoneOn instPreorder instPow Set.Ici	—	rpow_le_rpow
monotone_rpow_of_base_ge_one 📖	mathematical	Real instLE instOne	Monotone instPreorder instPow	—	lt_or_eq_of_le StrictMono.monotone strictMono_rpow_of_base_gt_one one_rpow
mul_log_eq_log_iff 📖	mathematical	Real instLT instZero	instMul log instPow	—	log_injOn_pos rpow_pos_of_pos log_rpow
mul_rpow 📖	mathematical	Real instLE instZero	instPow instMul	—	rpow_def_of_nonneg mul_nonneg IsOrderedRing.toPosMulMono instIsOrderedRing rpow_zero mul_one NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass log_mul add_mul Distrib.rightDistribClass exp_add rpow_def_of_pos LE.le.lt_of_ne'
norm_rpow_of_nonneg 📖	mathematical	Real instLE instZero	Norm.norm norm instPow	—	abs_rpow_of_nonneg
one_le_rpow 📖	mathematical	Real instLE instOne instZero	instPow	—	one_rpow rpow_le_rpow zero_le_one instZeroLEOneClass
one_le_rpow_of_pos_of_le_one_of_nonpos 📖	mathematical	Real instLT instZero instLE instOne	instPow	—	rpow_zero rpow_le_rpow_of_exponent_ge
one_lt_rpow 📖	mathematical	Real instLT instOne instZero	instPow	—	one_rpow rpow_lt_rpow zero_le_one instZeroLEOneClass
one_lt_rpow_iff 📖	mathematical	Real instLE instZero	instLT instOne instPow	—	LE.le.eq_or_lt em rpow_zero LT.lt.not_gt zero_lt_one' instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike zero_rpow one_lt_rpow_iff_of_pos
one_lt_rpow_iff_of_pos 📖	mathematical	Real instLT instZero	instOne instPow	—	rpow_def_of_pos one_lt_exp_iff mul_pos_iff AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_lt_of_covariant_le log_pos_iff LT.lt.le log_neg_iff
one_lt_rpow_of_pos_of_lt_one_of_neg 📖	mathematical	Real instLT instZero instOne	instPow	—	rpow_zero rpow_lt_rpow_of_exponent_gt
one_rpow 📖	mathematical	—	Real instPow instOne	—	Complex.one_cpow
pi_rpow_zero 📖	mathematical	—	Real Pi.instPow instPow instZero Pi.instOne instOne	—	rpow_zero
pow_le_iff_le_log 📖	mathematical	Real instLT instZero	instLE Monoid.toNatPow instMonoid instMul instNatCast log	—	rpow_le_iff_le_log rpow_natCast
pow_le_of_le_log 📖	mathematical	Real instLT instZero instLE log instMul instNatCast	Monoid.toNatPow instMonoid	—	rpow_le_of_le_log rpow_natCast
pow_lt_iff_lt_log 📖	mathematical	Real instLT instZero	Monoid.toNatPow instMonoid instMul instNatCast log	—	rpow_lt_iff_lt_log rpow_natCast
pow_lt_of_lt_log 📖	mathematical	Real instLT instZero log instMul instNatCast	Monoid.toNatPow instMonoid	—	rpow_lt_of_lt_log rpow_natCast
pow_rpow_inv_natCast 📖	mathematical	Real instLE instZero	instPow Monoid.toNatPow instMonoid instInv instNatCast	—	Nat.cast_ne_zero RCLike.charZero_rclike rpow_natCast rpow_mul mul_inv_cancel₀ rpow_one
rpow_add 📖	mathematical	Real instLT instZero	instPow instAdd instMul	—	rpow_def_of_pos mul_add Distrib.leftDistribClass exp_add
rpow_add' 📖	mathematical	Real instLE instZero	instPow instAdd instMul	—	LE.le.eq_or_lt zero_rpow zero_eq_mul NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass not_and_or zero_add rpow_add
rpow_add_intCast 📖	mathematical	—	Real instPow instAdd instIntCast instMul DivInvMonoid.toZPow instDivInvMonoid	—	rpow_def Complex.ofReal_add Complex.cpow_add Complex.ofReal_ne_zero Complex.ofReal_intCast Complex.cpow_intCast Complex.ofReal_zpow mul_comm Complex.re_ofReal_mul
rpow_add_intCast' 📖	mathematical	Real instLE instZero	instPow instAdd instIntCast instMul DivInvMonoid.toZPow instDivInvMonoid	—	rpow_add' rpow_intCast
rpow_add_natCast 📖	mathematical	—	Real instPow instAdd instNatCast instMul Monoid.toNatPow instMonoid	—	Int.cast_natCast zpow_natCast rpow_add_intCast
rpow_add_natCast' 📖	mathematical	Real instLE instZero	instPow instAdd instNatCast instMul Monoid.toNatPow instMonoid	—	rpow_add' rpow_natCast
rpow_add_of_nonneg 📖	mathematical	Real instLE instZero	instPow instAdd instMul	—	LE.le.eq_or_lt zero_add rpow_zero one_mul rpow_add' ne_of_gt add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
rpow_add_one 📖	mathematical	—	Real instPow instAdd instOne instMul	—	Nat.cast_one pow_one rpow_add_natCast
rpow_add_one' 📖	mathematical	Real instLE instZero	instPow instAdd instOne instMul	—	rpow_add' rpow_one
rpow_def 📖	mathematical	—	Real instPow Complex.re Complex Complex.instPow Complex.ofReal	—	—
rpow_def_of_neg 📖	mathematical	Real instLT instZero	instPow instMul exp log cos pi	—	rpow_def Complex.cpow_def Complex.ofReal_eq_zero ne_of_lt Complex.norm_real abs_of_neg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid log_neg_eq_log Complex.arg_ofReal_of_neg Complex.ofReal_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Complex.exp_add_mul_I Complex.ofReal_exp Complex.ofReal_cos Complex.ofReal_sin mul_add Distrib.leftDistribClass mul_assoc Complex.add_re Complex.ofReal_re Complex.mul_re Complex.I_re Complex.ofReal_im Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero
rpow_def_of_nonneg 📖	mathematical	Real instLE instZero	instPow decidableEq instOne exp instMul log	—	Complex.ofReal_log Complex.ofReal_mul
rpow_def_of_nonpos 📖	mathematical	Real instLE instZero	instPow decidableEq instOne instMul exp log cos pi	—	Complex.cpow_zero Complex.zero_cpow rpow_def_of_neg lt_of_le_of_ne
rpow_def_of_pos 📖	mathematical	Real instLT instZero	instPow exp instMul log	—	rpow_def_of_nonneg le_of_lt ne_of_gt
rpow_div_two_eq_sqrt 📖	mathematical	Real instLE instZero	instPow DivInvMonoid.toDiv instDivInvMonoid instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sqrt	—	Nat.instAtLeastTwoHAddOfNat sqrt_eq_rpow rpow_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Nat.cast_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one
rpow_eq_pow 📖	mathematical	—	rpow Real instPow	—	—
rpow_eq_zero 📖	mathematical	Real instLE instZero	instPow	—	—
rpow_eq_zero_iff_of_nonneg 📖	mathematical	Real instLE instZero	instPow	—	rpow_def_of_nonneg NeZero.charZero_one RCLike.charZero_rclike
rpow_intCast 📖	mathematical	—	Real instPow instIntCast DivInvMonoid.toZPow instDivInvMonoid	—	Complex.cpow_intCast
rpow_intCast_mul 📖	mathematical	Real instLE instZero	instPow instMul instIntCast DivInvMonoid.toZPow instDivInvMonoid	—	rpow_mul rpow_intCast
rpow_inv_eq 📖	mathematical	Real instLE instZero	instPow instInv	—	rpow_nonneg rpow_inv_rpow
rpow_inv_le_iff_of_neg 📖	mathematical	Real instLT instZero	instLE instPow instInv	—	rpow_le_rpow_iff_of_neg rpow_pos_of_pos rpow_inv_rpow le_of_lt LT.lt.ne
rpow_inv_le_iff_of_pos 📖	mathematical	Real instLE instZero instLT	instPow instInv	—	rpow_le_rpow_iff rpow_nonneg rpow_inv_rpow ne_of_gt
rpow_inv_log 📖	mathematical	Real instLT instZero	instPow instInv log exp instOne	—	rpow_def_of_pos mul_inv_cancel₀ log_ne_zero LT.lt.ne' Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg instIsStrictOrderedRing neg_neg_of_pos instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing
rpow_inv_log_le_exp_one 📖	mathematical	—	Real instLE instPow instInv log exp instOne	—	le_abs_self abs_rpow_le_abs_rpow log_abs LE.le.eq_or_lt' abs_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add log_zero inv_zero rpow_zero instZeroLEOneClass rpow_def_of_pos exp_monotone mul_inv_le_one
rpow_inv_lt_iff_of_neg 📖	mathematical	Real instLT instZero	instPow instInv	—	rpow_lt_rpow_iff_of_neg rpow_pos_of_pos rpow_inv_rpow le_of_lt LT.lt.ne
rpow_inv_lt_iff_of_pos 📖	mathematical	Real instLE instZero instLT	instPow instInv	—	lt_iff_lt_of_le_iff_le le_rpow_inv_iff_of_pos
rpow_inv_natCast_pow 📖	mathematical	Real instLE instZero	Monoid.toNatPow instMonoid instPow instInv instNatCast	—	Nat.cast_ne_zero RCLike.charZero_rclike rpow_natCast rpow_mul inv_mul_cancel₀ rpow_one
rpow_inv_rpow 📖	mathematical	Real instLE instZero	instPow instInv	—	rpow_mul inv_mul_cancel₀ rpow_one
rpow_le_iff_le_log 📖	mathematical	Real instLT instZero	instLE instPow instMul log	—	log_le_log_iff rpow_pos_of_pos log_rpow
rpow_le_of_le_log 📖	mathematical	Real instLT instZero instLE log instMul	instPow	—	le_or_gt LE.le.trans LT.lt.le rpow_pos_of_pos le_rpow_iff_log_le
rpow_le_one 📖	mathematical	Real instLE instZero instOne	instPow	—	one_rpow rpow_le_rpow
rpow_le_one_iff_of_pos 📖	mathematical	Real instLT instZero	instLE instPow instOne	—	rpow_def_of_pos exp_le_one_iff mul_nonpos_iff IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing IsStrictOrderedRing.toPosMulStrictMono IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid log_nonneg_iff log_nonpos_iff LT.lt.le
rpow_le_one_of_one_le_of_nonpos 📖	mathematical	Real instLE instOne instZero	instPow	—	rpow_zero rpow_le_rpow_of_exponent_le
rpow_le_rpow 📖	mathematical	Real instLE instZero	instPow	—	eq_or_lt_of_le le_refl rpow_zero le_of_lt rpow_lt_rpow
rpow_le_rpow_iff 📖	mathematical	Real instLE instZero instLT	instPow	—	le_iff_le_iff_lt_iff_lt rpow_lt_rpow_iff
rpow_le_rpow_iff_of_neg 📖	mathematical	Real instLT instZero	instLE instPow	—	le_iff_le_iff_lt_iff_lt rpow_lt_rpow_iff_of_neg
rpow_le_rpow_left_iff 📖	mathematical	Real instLT instOne	instLE instPow	—	lt_trans zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike log_le_log_iff rpow_pos_of_pos log_rpow mul_le_mul_iff_left₀ IsOrderedRing.toMulPosMono instIsOrderedRing MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing log_pos
rpow_le_rpow_left_iff_of_base_lt_one 📖	mathematical	Real instLT instZero instOne	instLE instPow	—	log_le_log_iff rpow_pos_of_pos log_rpow mul_le_mul_right_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le log_neg
rpow_le_rpow_of_exponent_ge 📖	mathematical	Real instLT instZero instLE instOne	instPow	—	rpow_def_of_pos exp_le_exp mul_le_mul_of_nonpos_left AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono instIsOrderedRing covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le log_nonpos le_of_lt
rpow_le_rpow_of_exponent_ge' 📖	mathematical	Real instLE instZero instOne	instPow	—	rpow_le_rpow_of_exponent_ge_of_imp le_antisymm LE.le.trans_eq
rpow_le_rpow_of_exponent_ge_of_imp 📖	mathematical	Real instLE instZero instOne	instPow	—	eq_or_lt_of_le eq_or_ne le_refl zero_rpow zero_rpow_nonneg rpow_le_rpow_of_exponent_ge
rpow_le_rpow_of_exponent_le 📖	mathematical	Real instLE instOne	instPow	—	rpow_def_of_pos lt_of_lt_of_le zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike exp_le_exp mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono instIsOrderedRing log_nonneg
rpow_le_rpow_of_exponent_le_or_ge 📖	mathematical	Real instLE instOne instLT instZero	instPow	—	rpow_le_rpow_of_exponent_le rpow_le_rpow_of_exponent_ge
rpow_le_rpow_of_exponent_nonpos 📖	mathematical	Real instLT instZero instLE	instPow	—	rpow_le_rpow_of_nonpos
rpow_le_rpow_of_nonpos 📖	mathematical	Real instLT instZero instLE	instPow	—	LT.lt.trans_le inv_le_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono rpow_pos_of_pos rpow_neg le_of_lt rpow_le_rpow neg_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
rpow_le_self_of_le_one 📖	mathematical	Real instLE instZero instOne	instPow	—	rpow_one rpow_le_rpow_of_exponent_ge_of_imp LT.lt.ne' LT.lt.trans_le one_pos instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
rpow_le_self_of_one_le 📖	mathematical	Real instLE instOne	instPow	—	rpow_one rpow_le_rpow_of_exponent_le
rpow_left_inj 📖	mathematical	Real instLE instZero	instPow	—	Set.InjOn.eq_iff rpow_left_injOn
rpow_left_injOn 📖	mathematical	—	Set.InjOn Real instPow setOf instLE instZero	—	rpow_one mul_inv_cancel₀ rpow_mul
rpow_lt_iff_lt_log 📖	mathematical	Real instLT instZero	instPow instMul log	—	log_lt_log_iff rpow_pos_of_pos log_rpow
rpow_lt_of_lt_log 📖	mathematical	Real instLT instZero log instMul	instPow	—	le_or_gt LE.le.trans_lt rpow_pos_of_pos lt_rpow_iff_log_lt
rpow_lt_one 📖	mathematical	Real instLE instZero instLT instOne	instPow	—	one_rpow rpow_lt_rpow
rpow_lt_one_iff 📖	mathematical	Real instLE instZero	instLT instPow instOne	—	LE.le.eq_or_lt em rpow_zero instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike zero_rpow rpow_lt_one_iff_of_pos LT.lt.ne
rpow_lt_one_iff' 📖	mathematical	Real instLE instZero instLT	instPow instOne	—	rpow_lt_rpow_iff zero_le_one instZeroLEOneClass one_rpow
rpow_lt_one_iff_of_pos 📖	mathematical	Real instLT instZero	instPow instOne	—	rpow_def_of_pos exp_lt_one_iff mul_neg_iff IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd log_pos_iff LT.lt.le log_neg_iff
rpow_lt_one_of_one_lt_of_neg 📖	mathematical	Real instLT instOne instZero	instPow	—	rpow_zero rpow_lt_rpow_of_exponent_lt
rpow_lt_rpow 📖	mathematical	Real instLE instZero instLT	instPow	—	le_iff_eq_or_lt zero_rpow ne_of_gt rpow_pos_of_pos rpow_def_of_pos lt_trans exp_lt_exp mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing log_lt_log
rpow_lt_rpow_iff 📖	mathematical	Real instLE instZero instLT	instPow	—	lt_imp_lt_of_le_imp_le rpow_le_rpow le_of_lt rpow_lt_rpow
rpow_lt_rpow_iff_of_neg 📖	mathematical	Real instLT instZero	instPow	—	lt_imp_lt_of_le_imp_le rpow_le_rpow_of_nonpos LT.lt.le rpow_lt_rpow_of_neg
rpow_lt_rpow_left_iff 📖	mathematical	Real instLT instOne	instPow	—	lt_iff_not_ge rpow_le_rpow_left_iff
rpow_lt_rpow_left_iff_of_base_lt_one 📖	mathematical	Real instLT instZero instOne	instPow	—	lt_iff_not_ge rpow_le_rpow_left_iff_of_base_lt_one
rpow_lt_rpow_of_exponent_gt 📖	mathematical	Real instLT instZero instOne	instPow	—	rpow_def_of_pos exp_lt_exp mul_lt_mul_of_neg_left AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le log_neg
rpow_lt_rpow_of_exponent_lt 📖	mathematical	Real instLT instOne	instPow	—	rpow_def_of_pos lt_trans zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike exp_lt_exp mul_lt_mul_of_pos_left IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing log_pos
rpow_lt_rpow_of_exponent_neg 📖	mathematical	Real instLT instZero	instPow	—	rpow_lt_rpow_of_neg
rpow_lt_rpow_of_neg 📖	mathematical	Real instLT instZero	instPow	—	LT.lt.trans inv_lt_inv₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono rpow_pos_of_pos rpow_neg le_of_lt rpow_lt_rpow neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
rpow_lt_self_of_lt_one 📖	mathematical	Real instLT instZero instOne	instPow	—	rpow_one rpow_lt_rpow_of_exponent_gt
rpow_lt_self_of_one_lt 📖	mathematical	Real instLT instOne	instPow	—	rpow_one rpow_lt_rpow_of_exponent_lt
rpow_max 📖	mathematical	Real instLE instZero	instPow instMax	—	le_total max_eq_right rpow_le_rpow max_eq_left
rpow_mul 📖	mathematical	Real instLE instZero	instPow instMul	—	Complex.ofReal_cpow rpow_nonneg Complex.ofReal_mul Complex.cpow_mul Complex.ofReal_log IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid le_of_lt pi_pos
rpow_mul_intCast 📖	mathematical	Real instLE instZero	instPow instMul instIntCast DivInvMonoid.toZPow instDivInvMonoid	—	rpow_mul rpow_intCast
rpow_mul_natCast 📖	mathematical	Real instLE instZero	instPow instMul instNatCast Monoid.toNatPow instMonoid	—	rpow_mul rpow_natCast
rpow_natCast 📖	mathematical	—	Real instPow instNatCast Monoid.toNatPow instMonoid	—	Int.cast_natCast zpow_natCast rpow_intCast
rpow_natCast_mul 📖	mathematical	Real instLE instZero	instPow instMul instNatCast Monoid.toNatPow instMonoid	—	rpow_mul rpow_natCast
rpow_ne_zero 📖	—	Real instLE instZero	—	—	—
rpow_neg 📖	mathematical	Real instLE instZero	instPow instNeg instInv	—	rpow_def_of_nonneg inv_one neg_zero inv_zero mul_neg exp_neg
rpow_neg_eq_inv_rpow 📖	mathematical	—	Real instPow instNeg instInv	—	Complex.ofReal_neg Complex.cpow_neg Complex.inv_re Complex.ofReal_inv Complex.inv_cpow_eq_ite Complex.conj_ofReal map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Complex.normSq_conj
rpow_neg_natCast 📖	mathematical	—	Real instPow instNeg instNatCast DivInvMonoid.toZPow instDivInvMonoid	—	rpow_intCast Int.cast_neg Int.cast_natCast
rpow_neg_ofNat 📖	mathematical	—	Real instPow instNeg DivInvMonoid.toZPow instDivInvMonoid	—	rpow_neg_natCast
rpow_neg_one 📖	mathematical	—	Real instPow instNeg instOne instInv	—	rpow_neg_eq_inv_rpow rpow_one
rpow_nonneg 📖	mathematical	Real instLE instZero	instPow	—	rpow_def_of_nonneg instZeroLEOneClass le_of_lt exp_pos
rpow_ofNat 📖	mathematical	—	Real instPow Monoid.toNatPow instMonoid	—	rpow_natCast
rpow_of_add_eq 📖	mathematical	Real instLE instZero instAdd	instPow instMul	—	rpow_add'
rpow_one 📖	mathematical	—	Real instPow instOne	—	Complex.cpow_one
rpow_one_add' 📖	mathematical	Real instLE instZero	instPow instAdd instOne instMul	—	rpow_add' rpow_one
rpow_one_sub' 📖	mathematical	Real instLE instZero	instPow instSub instOne DivInvMonoid.toDiv instDivInvMonoid	—	rpow_sub' rpow_one
rpow_pos_of_pos 📖	mathematical	Real instLT instZero	instPow	—	rpow_def_of_pos exp_pos
rpow_pow_comm 📖	mathematical	Real instLE instZero	Monoid.toNatPow instMonoid instPow	—	rpow_mul mul_comm
rpow_right_inj 📖	mathematical	Real instLT instZero	instPow	—	Ne.lt_or_gt StrictAnti.injective strictAnti_rpow_of_base_lt_one StrictMono.injective strictMono_rpow_of_base_gt_one
rpow_rpow_inv 📖	mathematical	Real instLE instZero	instPow instInv	—	rpow_mul mul_inv_cancel₀ rpow_one
rpow_sub 📖	mathematical	Real instLT instZero	instPow instSub DivInvMonoid.toDiv instDivInvMonoid	—	sub_eq_add_neg rpow_add rpow_neg le_of_lt div_eq_mul_inv
rpow_sub' 📖	mathematical	Real instLE instZero	instPow instSub DivInvMonoid.toDiv instDivInvMonoid	—	sub_eq_add_neg rpow_add' rpow_neg div_eq_mul_inv
rpow_sub_intCast 📖	mathematical	—	Real instPow instSub instIntCast DivInvMonoid.toDiv instDivInvMonoid DivInvMonoid.toZPow	—	Int.cast_neg zpow_neg rpow_add_intCast
rpow_sub_intCast' 📖	mathematical	Real instLE instZero	instPow instSub instIntCast DivInvMonoid.toDiv instDivInvMonoid DivInvMonoid.toZPow	—	rpow_sub' rpow_intCast
rpow_sub_natCast 📖	mathematical	—	Real instPow instSub instNatCast DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid	—	Int.cast_natCast zpow_natCast rpow_sub_intCast
rpow_sub_natCast' 📖	mathematical	Real instLE instZero	instPow instSub instNatCast DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid	—	rpow_sub' rpow_natCast
rpow_sub_one 📖	mathematical	—	Real instPow instSub instOne DivInvMonoid.toDiv instDivInvMonoid	—	Nat.cast_one pow_one rpow_sub_natCast
rpow_sub_one' 📖	mathematical	Real instLE instZero	instPow instSub instOne DivInvMonoid.toDiv instDivInvMonoid	—	rpow_sub' rpow_one
rpow_sum_of_nonneg 📖	mathematical	Real instLE instZero	instPow Finset.sum instAddCommMonoid Finset.prod instCommMonoid	—	Finset.cons_induction Finset.sum_empty Finset.prod_empty rpow_zero Finset.sum_cons Finset.prod_cons Finset.forall_mem_cons rpow_add_of_nonneg Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
rpow_sum_of_pos 📖	mathematical	Real instLT instZero	instPow Finset.sum instAddCommMonoid Finset.prod instCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass rpow_zero rpow_add
rpow_two 📖	mathematical	—	Real instPow instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat rpow_ofNat
rpow_zero 📖	mathematical	—	Real instPow instZero instOne	—	Complex.cpow_zero
rpow_zero_pos 📖	mathematical	—	Real instLT instZero instPow	—	rpow_zero instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
rpow_zpow_comm 📖	mathematical	Real instLE instZero	DivInvMonoid.toZPow instDivInvMonoid instPow	—	rpow_mul mul_comm
self_le_rpow_of_le_one 📖	mathematical	Real instLE instZero instOne	instPow	—	rpow_one rpow_le_rpow_of_exponent_ge_of_imp one_ne_zero NeZero.charZero_one RCLike.charZero_rclike
self_le_rpow_of_one_le 📖	mathematical	Real instLE instOne	instPow	—	rpow_one rpow_le_rpow_of_exponent_le
self_lt_rpow_of_lt_one 📖	mathematical	Real instLT instZero instOne	instPow	—	rpow_one rpow_lt_rpow_of_exponent_gt
self_lt_rpow_of_one_lt 📖	mathematical	Real instLT instOne	instPow	—	rpow_one rpow_lt_rpow_of_exponent_lt
sqrt_eq_rpow 📖	mathematical	—	sqrt Real instPow DivInvMonoid.toDiv instDivInvMonoid instOne instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat le_or_gt mul_self_inj_of_nonneg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass instIsStrictOrderedRing sqrt_nonneg rpow_nonneg mul_self_sqrt sq rpow_natCast rpow_mul one_div inv_mul_cancel₀ RCLike.charZero_rclike rpow_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left sqrt_eq_zero_of_nonpos LT.lt.le rpow_def_of_neg cos_pi_div_two MulZeroClass.mul_zero
strictAntiOn_rpow_Ioi_of_exponent_neg 📖	mathematical	Real instLT instZero	StrictAntiOn instPreorder instPow Set.Ioi	—	rpow_lt_rpow_of_neg
strictAnti_rpow_of_base_lt_one 📖	mathematical	Real instLT instZero instOne	StrictAnti instPreorder instPow	—	rpow_def_of_pos StrictMono.comp_strictAnti exp_strictMono StrictMono.const_mul_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le strictMono_id log_neg
strictMonoOn_rpow_Ici_of_exponent_pos 📖	mathematical	Real instLT instZero	StrictMonoOn instPreorder instPow Set.Ici	—	rpow_lt_rpow
strictMono_rpow_of_base_gt_one 📖	mathematical	Real instLT instOne	StrictMono instPreorder instPow	—	rpow_def_of_pos LT.lt.trans zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike StrictMono.comp exp_strictMono StrictMono.const_mul IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing strictMono_id log_pos
zero_rpow 📖	mathematical	—	Real instPow instZero	—	Complex.zero_cpow
zero_rpow_eq_iff 📖	mathematical	—	Real instPow instZero instOne	—	Complex.cpow_zero Complex.zero_cpow Complex.ofReal_ne_zero zero_rpow rpow_zero
zero_rpow_le_one 📖	mathematical	—	Real instLE instPow instZero instOne	—	rpow_zero zero_rpow instZeroLEOneClass
zero_rpow_nonneg 📖	mathematical	—	Real instLE instZero instPow	—	rpow_zero instZeroLEOneClass zero_rpow
zpow_le_iff_le_log 📖	mathematical	Real instLT instZero	instLE DivInvMonoid.toZPow instDivInvMonoid instMul instIntCast log	—	rpow_le_iff_le_log rpow_intCast
zpow_le_of_le_log 📖	mathematical	Real instLT instZero instLE log instMul instIntCast	DivInvMonoid.toZPow instDivInvMonoid	—	rpow_le_of_le_log rpow_intCast
zpow_lt_iff_lt_log 📖	mathematical	Real instLT instZero	DivInvMonoid.toZPow instDivInvMonoid instMul instIntCast log	—	rpow_lt_iff_lt_log rpow_intCast
zpow_lt_of_lt_log 📖	mathematical	Real instLT instZero log instMul instIntCast	DivInvMonoid.toZPow instDivInvMonoid	—	rpow_lt_of_lt_log rpow_intCast

---

← Back to Index