R — Mathlib · SciLib

English

The image under frobenius of the roots of expand R p f sits inside f.roots.

Русский

Образ по Фробениусу корней expand_R(p,f) лежит в корнях f.

LaTeX

$$$(\expand_R\;p\;f)\ \text{roots}^{\text{toFinset}} \xrightarrow{\text{image}} f.\text{roots}^{\text{toFinset}}$$$

Lean4

/-- `PerfectClosure.R` is the relation `(n, x) ∼ (n + 1, x ^ p)` for `n : ℕ` and `x : K`.
`PerfectClosure K p` is the quotient by this relation. -/
@[mk_iff]
inductive R : ℕ × K → ℕ × K → Prop
  | intro : ∀ n x, PerfectClosure.R (n, x) (n + 1, frobenius K p x)

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