baseChange_dblZ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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