@[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 : ℤ} :
theorem
fpow_le_one_of_nonpos
{K : Type u}
[discrete_linear_ordered_field K]
{p : K}
(hp : 1 ≤ p)
{z : ℤ} :
theorem
one_le_fpow_of_nonneg
{K : Type u}
[discrete_linear_ordered_field K]
{p : K}
(hp : 1 ≤ p)
{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} :
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} :
0 < x → x ≠ 1 → function.injective (has_pow.pow x)