liftAux_self_apply — Mathlib

English

If i = j and M is suitable, liftAux(i,i,p) x = x for all x ∈ L.

Русский

Если i = j и M удовлетворяет условиям, то liftAux(i,i,p) x = x для всех x ∈ L.

LaTeX

$$$liftAux(i,i,p)(x) = x$ for all x ∈ L$$

Lean4

@[simp]
theorem liftAux_self_apply [ExpChar L p] [PerfectRing L p] (x : L) : liftAux i i p x = x := by
  rw [liftAux, Classical.choose_spec (lift_aux i p x), ← iterateFrobenius_def, ← iterateFrobeniusEquiv_apply,
    RingEquiv.symm_apply_apply]

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