PointClass — Mathlib

English

If u is a unit, then the projective class of u • P equals the class of P: ⟦u • P⟧ = ⟦P⟧.

Русский

Если u является обратимым элементом, то эквивалентность проектной точки не меняется: ⟦u • P⟧ = ⟦P⟧.

LaTeX

$$\llbracket u \cdot P \rrbracket = \llbracket P \rrbracket$$

Lean4

/-- The equivalence class of a projective point representative on a Weierstrass curve. -/
abbrev PointClass : Type r :=
  MulAction.orbitRel.Quotient Rˣ <| Fin 3 → R

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