map_dblU — Mathlib

English

Under a ring hom f, the image of dblU respects scalar action: map f of dblU(P) equals dblU of map f applied to P.

Русский

При отображении g через колено кольца сохраняется действие удвоения: map f(dblU(P)) = dblU(map f(P)).

LaTeX

$$$\big( W.map f \big).toProjective.dblU (f \circ P) = f\big( W.dblU P \big)$$$

Lean4

@[simp]
theorem map_dblU (f : F →+* K) (P : Fin 3 → F) : (W.map f).toProjective.dblU (f ∘ P) = f (W.dblU P) :=
  by
  simp only [dblU_eq]
  map_simp

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