baseChange_negDblY — Mathlib

English

(W'.baseChange B).toProjective.negDblY (f ∘ P) = f ((W'.baseChange A).toProjective.negDblY P)

Русский

Базовое изменение сохраняет negDblY: (W'.baseChange B).toProjective.negDblY (f ∘ P) = f ((W'.baseChange A).toProjective.negDblY P).

LaTeX

$$ (W'.baseChange B).toProjective.negDblY (f ∘ P) = f ((W'.baseChange A).toProjective.negDblY P) $$

Lean4

theorem baseChange_negDblY :
    (W'.baseChange B).toProjective.negDblY (f ∘ P) = f ((W'.baseChange A).toProjective.negDblY P) := by
  rw [← RingHom.coe_coe, ← map_negDblY, map_baseChange]

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