ext — Mathlib

English

Extensionality of IsAdjoinRoot: two instances are equal if their maps agree on all inputs.

Русский

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

LaTeX

$$ext (h' : IsAdjoinRoot S f) (eq : ∀ x, h.map x = h'.map x) : h = h'$$

Lean4

/-- Extensionality of the `IsAdjoinRoot` structure itself. See `IsAdjoinRootMonic.ext_elem`
for extensionality of the ring elements. -/
@[ext]
theorem ext (h' : IsAdjoinRoot S f) (eq : h.root = h'.root) : h = h' :=
  h.ext_map h' (fun x => by rw [← h.aeval_root_eq_map, ← h'.aeval_root_eq_map, eq])

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