map_negY

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Affine.map_negY

English

The negY operation commutes with any ring homorphism: applying f to the arguments and then negY equals applying negY after mapping.

Русский

Операция negY commute с отображением: f(negY(x,y)) = negY(f(x), f(y)).

LaTeX

$$$ (W'.map f).toAffine.negY (f x) (f y) = f (W'.negY x y) $$$

Lean4

theorem map_negY : (W'.map f).toAffine.negY (f x) (f y) = f (W'.negY x y) :=
  by
  simp only [negY]
  map_simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru