instSetoidForallFinOfNatNat — Mathlib

English

The setoid on Fin 3 → R is the orbit relation under the action of Units(R) by coordinatewise multiplication.

Русский

На множестве Fin 3 → R задано множество эквивалентности как орбитальное отношение действия единиц R на вектор по координатам.

LaTeX

$$P \approx Q \iff \exists u \in R^\times, Q = u • P$$

Lean4

/-- The equivalence setoid for a projective point representative on a Weierstrass curve. -/
@[reducible]
scoped instance : Setoid <| Fin 3 → R :=
  MulAction.orbitRel Rˣ <| Fin 3 → R

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