English
Under the bijection, the representative has the value x^{p^n}.
Русский
При биекции представителю соответствует значение x^{p^n}.
LaTeX
$$$\text{RootsExpandPowEquivRoots_apply }(p,f,n,x) : (\text{root}) = x^{p^n}$$$
Lean4
/-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
a bijection from the set of roots of `Polynomial.expand R p f` to the set of roots of `f`.
It's given by `x ↦ x ^ p`, see `rootsExpandEquivRoots_apply`. -/
noncomputable def rootsExpandEquivRoots : (expand R p f).roots.toFinset ≃ f.roots.toFinset :=
((frobeniusEquiv R p).image _).trans <|
.setCongr <|
show _ '' setOf (· ∈ _) = setOf (· ∈ _) by
classical
simp_rw [← roots_expand_image_frobenius (p := p) (f := f), Finset.mem_val, Finset.setOf_mem, Finset.coe_image,
RingEquiv.toEquiv_eq_coe, EquivLike.coe_coe, frobeniusEquiv_apply]
