mapFun — Mathlib

English

If a function f is injective, then the Witt vector mapFun f : 𝕎 α → 𝕎 β is injective.

Русский

Если функция f инъективна, то отображение WittVector.mapFun f : 𝕎 α → 𝕎 β инъективно.

LaTeX

$$$\\operatorname{Injective}(\\mathrm{WittVector.mapFun}\\, f)$$$

Lean4

/-- `f : α → β` induces a map from `𝕎 α` to `𝕎 β` by applying `f` componentwise.
If `f` is a ring homomorphism, then so is `f`, see `WittVector.map f`. -/
def mapFun (f : α → β) : 𝕎 α → 𝕎 β := fun x => mk _ (f ∘ x.coeff)

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