baseChange_negY — Mathlib

English

NegY commutes with base change: (W'.baseChange B).toProjective.negY (f ∘ P) = f ((W'.baseChange A).toProjective.negY P).

Русский

Сохранение negY при базовом изменении: (W'.baseChange B).toProjective.negY (f ∘ P) = f ((W'.baseChange A).toProjective.negY P).

LaTeX

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

Lean4

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

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