solution_pow — Mathlib

English

There exists x in k such that x^{p-1} equals a2.coeff 0 divided by a1.coeff 0, in an algebraically closed field of characteristic p.

Русский

Существует элемент x в k такой, что x^{p-1} равно a2.coeff 0 / a1.coeff 0, в алгебраически замкнутом поле характеристики p.

LaTeX

$$$\exists x \in k:\; x^{p-1} = \dfrac{a_2.coeff\,0}{a_1.coeff\,0}$$$

Lean4

theorem solution_pow (a₁ a₂ : 𝕎 k) : ∃ x : k, x ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0 :=
  IsAlgClosed.exists_pow_nat_eq _ <| tsub_pos_of_lt hp.out.one_lt

Похожие утверждения