map_repr — Mathlib

English

Let h be an IsAdjoinRoot S f. Then the representation map repr and the canonical map map are mutual inverses on S, i.e., for every x in S, h.map (h.repr x) = x.

Русский

Пусть h — IsAdjoinRoot S f. Тогда отображение представления repr и каноническое отображение map взаимно обратны на S: для каждого x∈S выполняется h.map (h.repr x) = x.

LaTeX

$$$\forall x \in S,\ h.map\bigl(h.repr(x)\bigr) = x$$$

Lean4

@[simp]
theorem map_repr (x : S) : h.map (h.repr x) = x :=
  (h.map_surjective x).choose_spec

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