baseChange_addXYZ — Mathlib

English

Base change is compatible with addXYZ: (W'.baseChange B).toJacobian.addXYZ (f ∘ P) (f ∘ Q) = f ∘ (W'.baseChange A).toJacobian.addXYZ P Q.

Русский

Базовое изменение совместимо с addXYZ: (W'.baseChange B).toJacobian.addXYZ (f ∘ P) (f ∘ Q) = f ∘ (W'.baseChange A).toJacobian.addXYZ P Q.

LaTeX

$$$ (W'.baseChange B).toJacobian.addXYZ (f \circ P) (f \circ Q) = f \circ (W'.baseChange A).toJacobian.addXYZ P Q $$$

Lean4

theorem baseChange_addXYZ :
    (W'.baseChange B).toJacobian.addXYZ (f ∘ P) (f ∘ Q) = f ∘ (W'.baseChange A).toJacobian.addXYZ P Q := by
  rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]

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