Theorems · Definition · commutative algebra

WittVector.mapFun

{p : ℕ} → {α : Type u_3} → {β : Type u_4} → (α → β) → WittVector p α → WittVector p β

f : α → β induces a map from 𝕎 α to 𝕎 β by applying f componentwise. If f is a ring homomorphism, then so is f, see WittVector.map f.

Defined in

Mathlib.RingTheory.WittVector.Basic

Cited by

13 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms