map_addX — Mathlib

English

The addZ coordinate also commutes with ring homomorphisms: (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_addX : (W'.map f).toProjective.addX (f ∘ P) (f ∘ Q) = f (W'.addX P Q) :=
  by
  simp only [addX]
  map_simp

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