@[simp]
theorem
ring_hom.map_fpow
{K : Type u_1}
{L : Type u_2}
[division_ring K]
[division_ring L]
(f : K →+* L)
(a : K)
(n : ℤ) :
theorem
fpow_nonneg_of_nonneg
{K : Type u}
[discrete_linear_ordered_field K]
{a : K}
(ha : 0 ≤ a)
(z : ℤ) :
theorem
fpow_pos_of_pos
{K : Type u}
[discrete_linear_ordered_field K]
{a : K}
(ha : 0 < a)
(z : ℤ) :
theorem
fpow_le_of_le
{K : Type u}
[discrete_linear_ordered_field K]
{x : K}
(hx : 1 ≤ x)
{a b : ℤ}
(h : a ≤ b) :
theorem
fpow_le_one_of_nonpos
{K : Type u}
[discrete_linear_ordered_field K]
{p : K}
(hp : 1 ≤ p)
{z : ℤ}
(hz : z ≤ 0) :
theorem
one_le_fpow_of_nonneg
{K : Type u}
[discrete_linear_ordered_field K]
{p : K}
(hp : 1 ≤ p)
{z : ℤ}
(hz : 0 ≤ z) :
theorem
one_lt_pow
{K : Type u_1}
[linear_ordered_semiring K]
{p : K}
(hp : 1 < p)
{n : ℕ}
(a : 1 ≤ n) :
theorem
one_lt_fpow
{K : Type u_1}
[discrete_linear_ordered_field K]
{p : K}
(hp : 1 < p)
(z : ℤ)
(a : 0 < z) :
theorem
nat.fpow_pos_of_pos
{K : Type u_1}
[discrete_linear_ordered_field K]
{p : ℕ}
(h : 0 < p)
(n : ℤ) :
theorem
nat.fpow_ne_zero_of_pos
{K : Type u_1}
[discrete_linear_ordered_field K]
{p : ℕ}
(h : 0 < p)
(n : ℤ) :
theorem
fpow_strict_mono
{K : Type u_1}
[discrete_linear_ordered_field K]
{x : K}
(hx : 1 < x) :
strict_mono (λ (n : ℤ), x ^ n)
@[simp]
theorem
fpow_lt_iff_lt
{K : Type u_1}
[discrete_linear_ordered_field K]
{x : K}
(hx : 1 < x)
{m n : ℤ} :
@[simp]
theorem
fpow_le_iff_le
{K : Type u_1}
[discrete_linear_ordered_field K]
{x : K}
(hx : 1 < x)
{m n : ℤ} :
@[simp]
theorem
pos_div_pow_pos
{K : Type u_1}
[discrete_linear_ordered_field K]
{a b : K}
(ha : 0 < a)
(hb : 0 < b)
(k : ℕ) :
@[simp]
theorem
div_pow_le
{K : Type u_1}
[discrete_linear_ordered_field K]
{a b : K}
(ha : 0 < a)
(hb : 1 ≤ b)
(k : ℕ) :
theorem
fpow_injective
{K : Type u_1}
[discrete_linear_ordered_field K]
{x : K}
(h₀ : 0 < x)
(h₁ : x ≠ 1) :