α : Type u
β : Type ?u.57127
inst✝¹ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
inst✝ : Nontrivial α
⊢ 0 < a ^ 0
α : Type u
β : Type ?u.57127
inst✝ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
⊢ 0 < a ^ 0
nontriviality
α : Type u
β : Type ?u.57127
inst✝¹ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
inst✝ : Nontrivial α
⊢ 0 < 1
α : Type u
β : Type ?u.57127
inst✝¹ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
inst✝ : Nontrivial α
⊢ 0 < a ^ 0
rw [pow_zero]
no goals
α : Type u
β : Type ?u.57127
inst✝¹ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
inst✝ : Nontrivial α
⊢ 0 < 1
exact zero_lt_one
α : Type u
β : Type ?u.57127
inst✝ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
n : ℕ
⊢ 0 < a * a ^ n
α : Type u
β : Type ?u.57127
inst✝ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
n : ℕ
⊢ 0 < a ^ (n + 1)
rw [pow_succ]
no goals
α : Type u
β : Type ?u.57127
inst✝ : StrictOrderedSemiring α
a b c d : α
H : 0 < a
n : ℕ
⊢ 0 < a * a ^ n
exact mul_pos H (pow_pos H _)