map_negY — Mathlib

English

Under a ring hom f, the negY maps compatibly with the Jacobian structure: map_negY states that applying map to the Jacobian and then negY equals applying negY after map to the arguments.

Русский

При гомоморфизме колец отображение map и функция negY согласованы на уровне Якобиана.

LaTeX

$$$$ (W'.map f).toJacobian.negY (f \\circ P) = f (W'.negY P) $$$$

Lean4

@[simp]
theorem map_negY : (W'.map f).toJacobian.negY (f ∘ P) = f (W'.negY P) :=
  by
  simp only [negY]
  map_simp

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