map_addXYZ — Mathlib

English

Let f: R → S be a ring hom and P, Q: Fin 3 → R. Then addXYZ is natural with respect to f: (W'.map f).toJacobian.addXYZ (f ∘ P) (f ∘ Q) = f ∘ (W'.addXYZ P Q).

Русский

Пусть f: R → S — кольцевой гомоморфизм и P, Q: Fin 3 → R. Тогда addXYZ естественно по отношению к f: (W'.map f).toJacobian.addXYZ (f ∘ P) (f ∘ Q) = f ∘ (W'.addXYZ P Q).

LaTeX

$$$ (W'.map f).toJacobian.addXYZ (f \circ P) (f \circ Q) = f ∘ (W'.addXYZ P Q) $$$

Lean4

@[simp]
theorem map_addXYZ : (W'.map f).toJacobian.addXYZ (f ∘ P) (f ∘ Q) = f ∘ addXYZ W' P Q := by
  simp only [addXYZ, map_addX, map_addY, map_addZ, comp_fin3]

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