repr — Mathlib

English

Represents a chosen representative polynomial that maps to a given element via h.map.

Русский

Задается выбранный представитель полинома, отображаемый через h.map.

LaTeX

$$def repr (x : S) : R[X] := (h.map x).choose$$

Lean4

/-- Choose an arbitrary representative so that `h.map (h.repr x) = x`.

If `f` is monic, use `IsAdjoinRootMonic.modByMonicHom` for a unique choice of representative.
-/
def repr (x : S) : R[X] :=
  (h.map_surjective x).choose

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