ext_ring_iff — Mathlib

English

Two continuous R-algebra morphisms f, g from R to A are equal if and only if they agree at the unit 1.

Русский

Два непрерывных гомоморфизма R-алгебры f,g из R в A равны тогда и только тогда, когда они совпадают на единице 1.

LaTeX

$$$f = g \\;\\Longleftrightarrow\\; f(1) = g(1).$$$

Lean4

theorem ext_ring_iff [TopologicalSpace R] {f g : R →A[R] A} : f = g ↔ f 1 = g 1 :=
  ⟨fun h => h ▸ rfl, fun _ => ext_ring⟩

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