natCast — Mathlib

English

The Witt vector map respects the unit, zero, addition, and multiplication together, giving a ring homomorphism 𝕎 R → 𝕎 S.

Русский

Отображение WittVector.map образует гомоморфизм кольца 𝕎 R → 𝕎 S, сохраняющий ноль, единицу, сложение и умножение.

LaTeX

$$$\\mathrm{WittVector.map}\\ f : 𝕎 R → 𝕎 S$ is a ring homomorphism$$

Lean4

theorem natCast (n : ℕ) : mapFun f (n : 𝕎 R) = n :=
  show mapFun f n.unaryCast = (n : WittVector p S) by induction n <;> simp [*, Nat.unaryCast, add, one, zero] <;> rfl

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