ext_map — Mathlib

English

Extensionality principle for IsAdjoinRoot: if h.map equals h'.map on all polynomials, then h = h'.

Русский

Принцип эктенсиальности IsAdjoinRoot: если для всех полиномов отображения совпадают, то структуры равны.

LaTeX

$$$\\forall x, \\; h.map x = h'.map x \\Rightarrow h = h'$$$

Lean4

/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
for extensionality of the ring elements. -/
theorem ext_map (h' : IsAdjoinRoot S f) (eq : ∀ x, h.map x = h'.map x) : h = h' :=
  by
  cases h; cases h'; congr
  exact AlgHom.ext eq

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