LeanPool.EcTateLean.FieldTheory.PerfectClosure

Imported Lean Pool material for LeanPool.EcTateLean.FieldTheory.PerfectClosure.

class ECTate.PerfectRing (R : Type u_1) [CommSemiring R] : Prop

A perfect ring is one where raising to the power of the ring characteristic is a bijection or a ring of char zero.

Note this is distinct from the mathlib version in that we allow char 0

• pth_power_bijective : ringChar R = 0 ∨ Function.Bijective fun (x : R) => x ^ ringChar R

theorem ECTate.PerfectRing.pth_power_bijective_of_char_nonzero {R : Type u_1} [CommSemiring R] [PerfectRing R] (h : ringChar R ≠ 0) : Function.Bijective fun (x : R) => x ^ ringChar R

noncomputable def ECTate.PerfectRing.pthRoot {R : Type u_1} [CommSemiring R] [PerfectRing R] : R → R

The inverse of the p-th power map on a perfect ring (the identity in characteristic zero).

Equations

• ECTate.PerfectRing.pthRoot = if h : ringChar R = 0 then id else Function.surjInv ⋯

theorem ECTate.PerfectRing.pthRoot_pow_char {R : Type u_1} [CommSemiring R] [PerfectRing R] (h : ringChar R ≠ 0) (x : R) : pthRoot x ^ ringChar R = x

theorem ECTate.PerfectRing.pthRoot_pow_eq {R : Type u_1} [CommSemiring R] {n : ℕ} [PerfectRing R] (x : R) : pthRoot x ^ n = x ^ (n / ringChar R) * pthRoot x ^ (n % ringChar R)

@[simp]

theorem ECTate.PerfectRing.pthRoot_zero {R : Type u_1} [CommSemiring R] [PerfectRing R] : pthRoot 0 = 0