baseChange_add — Mathlib

English

Negation and addition commute with a base change: the base-changed sum equals the base-change of the sum.

Русский

Сумма и отрицание сохраняются при базовом изменении: базированная сумма равна базированной сумме.

LaTeX

$$$(W'.baseChange K).toProjective.add (f \\circ P) (f \\circ Q) = f \\circ (W'.baseChange F).toProjective.add P Q$$$

Lean4

theorem baseChange_add [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K]
    [IsScalarTower R S K] (f : F →ₐ[S] K) {P Q : Fin 3 → F} (hP : (W'.baseChange F).toProjective.Nonsingular P)
    (hQ : (W'.baseChange F).toProjective.Nonsingular Q) :
    (W'.baseChange K).toProjective.add (f ∘ P) (f ∘ Q) = f ∘ (W'.baseChange F).toProjective.add P Q := by
  rw [← RingHom.coe_coe, ← WeierstrassCurve.Projective.map_add _ hP hQ, map_baseChange]

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