Commit 2023-12-19 15:21 ea02b9e2

View on Github →

feat: More rpow lemmas (#9108) A bunch of easy lemmas about Real.pow and the golf of existing lemmas with them. Also rename log_le_log to log_le_log_iff and log_le_log' to log_le_log. Those misnames caused several proofs to bother with side conditions they didn't need. From LeanAPAP

Estimated changes

deleted theorem Real.log_le_log'
modified theorem Real.log_le_log
added theorem Real.log_le_log_iff
modified theorem Real.log_lt_log
added theorem Real.eq_rpow_inv
added theorem Real.exp_one_pow
modified theorem Real.mul_rpow
deleted theorem Real.pow_nat_rpow_nat_inv
added theorem Real.rpow_add_int'
added theorem Real.rpow_add_nat'
added theorem Real.rpow_add_one'
added theorem Real.rpow_eq_zero
added theorem Real.rpow_intCast_mul
added theorem Real.rpow_inv_eq
added theorem Real.rpow_inv_rpow
added theorem Real.rpow_left_inj
added theorem Real.rpow_mul_intCast
added theorem Real.rpow_mul_natCast
added theorem Real.rpow_natCast_mul
modified theorem Real.rpow_nat_cast
deleted theorem Real.rpow_nat_inv_pow_nat
added theorem Real.rpow_one_add'
added theorem Real.rpow_one_sub'
added theorem Real.rpow_rpow_inv
added theorem Real.rpow_sub_int'
added theorem Real.rpow_sub_nat'
added theorem Real.rpow_sub_one'
added theorem Complex.exp_nsmul
added theorem Real.exp_nsmul