XYIdeal'_eq — Mathlib

English

For a nonsingular pair (x, y) on W, the unit representing the nonzero fractional ideal XYIdeal'(h) coincides with the standard XYIdeal attached to the point (x, y) via Y and X coordinates: XYIdeal'(h) = XYIdeal W x (C y).

Русский

Для невырожденной точки (x, y) на W единичный представитель дробного идеала XYIdeal'(h) совпадает с обычным XYIdeal, полученным из точки (x, y) через X и Y: XYIdeal'(h) = XYIdeal W x (C y).

LaTeX

$$$(XYIdeal'\\, h) = XYIdeal\\, W\\, x\\, (C\\, y)$$$

Lean4

theorem XYIdeal'_eq {x y : F} (h : W.Nonsingular x y) :
    (XYIdeal' h : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) = XYIdeal W x (C y) :=
  rfl

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