n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (deriv fun a => a ^ n)
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictConvexOn ℝ univ fun x => x ^ n
apply StrictMono.strictConvexOn_univ_of_deriv (continuous_pow n)
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono (deriv fun a => a ^ n)
rw [deriv_pow']
n : ℕ
hn : Even n
h : 0 < n
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
n : ℕ
hn : Even n
h : n ≠ 0
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
replace h := Nat.pos_of_ne_zero h
no goals
n : ℕ
hn : Even n
h : 0 < n
⊢ StrictMono fun x => ↑n * x ^ (n - 1)
exact StrictMono.const_mul (Odd.strictMono_pow <| Nat.Even.sub_odd h hn <| Nat.odd_iff.2 rfl)
  (Nat.cast_pos.2 h)