map_addXYZ — Mathlib

English

The mapping commutes with addition XYZ: (W'.map f).toProjective.addXYZ (f ∘ P) (f ∘ Q) = f ∘ addXYZ W' P Q.

Русский

Отображение сохраняет операцию сложения XYZ: (W'.map f).toProjective.addXYZ (f ∘ P) (f ∘ Q) = f ∘ addXYZ W' P Q.

LaTeX

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

Lean4

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

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