map_mk — Mathlib

English

For an injective semilinear map f: V →_σ W, the induced map on projective spaces sends mk K v hv to mk L (f v) with the appropriate nonzero condition.

Русский

Для инъективного полубиллинейного отображения f: V →_σ W отображение на проективном пространстве отправляет mk K v hv в mk L (f v) с соответствующим ненулевым условием.

LaTeX

$$$ \forall {f}, \ hf,\ map f hf (mk K v hv) = mk L (f v) (map_zero f \ arrow hf.ne hv) $$$

Lean4

theorem map_mk {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective f) (v : V) (hv : v ≠ 0) :
    map f hf (mk K v hv) = mk L (f v) (map_zero f ▸ hf.ne hv) :=
  rfl

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