hom_ext — Mathlib

English

Let R be a (possibly nonassociative) ring. If f and g are ring homomorphisms from Z[√d] to R and they coincide on √d, then f and g are equal.

Русский

Пусть R — кольцо (возможно неассоциативное). Если f и g — кольцевые гомоморфизмы из Z[√d] в R и они совпадают на √d, то f = g.

LaTeX

$$$\\forall d \\in \\mathbb{Z},\\ \\forall f,g:\\mathbb{Z}[\\sqrt{d}]\\to^+_*R,\\ f(\\sqrt{d})=g(\\sqrt{d})\\Rightarrow f=g.$$$

Lean4

@[ext]
theorem hom_ext [NonAssocRing R] {d : ℤ} (f g : ℤ√d →+* R) (h : f sqrtd = g sqrtd) : f = g :=
  by
  ext ⟨re_x, im_x⟩
  simp [decompose, h]

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