map_addU — Mathlib

English

The addZ coordinate respects the projection under a RingHom: (W'.map f).toProjective.addZ (f ∘ P) (f ∘ Q) = f(W'.addZ P Q).

Русский

Сложение по Z корректно отображается: (map f).addZ(P,Q) = f(addZ(P,Q)).

LaTeX

$$$(W'.map f).toProjective.addZ (f \circ P) (f \circ Q) = f (W'.addZ P Q)$$$

Lean4

@[simp]
theorem map_addU (f : F →+* K) (P Q : Fin 3 → F) : addU (f ∘ P) (f ∘ Q) = f (addU P Q) :=
  by
  simp only [addU]
  map_simp

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