English
The projection (Verschiebung) distributes over multiplication with Frobenius: Verschiebung(x · Frobenius(y)) = Verschiebung(x) · y.
Русский
Проекция (Verschiebung) распределяется по умножению с Frobenius: Verschiebung(x · Frobenius(y)) = Verschiebung(x) · y.
LaTeX
$$$ \operatorname{verschiebung}(x \cdot \operatorname{frobenius}(y)) = \operatorname{verschiebung}(x) \cdot y $$$
Lean4
/-- The “projection formula” for Frobenius and Verschiebung. -/
theorem verschiebung_mul_frobenius (x y : 𝕎 R) : verschiebung (x * frobenius y) = verschiebung x * y :=
by
have : IsPoly₂ p fun {R} [Rcr : CommRing R] x y ↦ verschiebung (x * frobenius y) :=
IsPoly.comp₂ (hg := verschiebung_isPoly) (hf :=
IsPoly₂.comp (hh := mulIsPoly₂) (hf := idIsPolyI' p) (hg := frobenius_isPoly p))
have : IsPoly₂ p fun {R} [CommRing R] x y ↦ verschiebung x * y :=
IsPoly₂.comp (hh := mulIsPoly₂) (hf := verschiebung_isPoly) (hg := idIsPolyI' p)
ghost_calc x y
rintro ⟨⟩ <;> ghost_simp [mul_assoc]
