map_adjoin_singleton — Mathlib

English

If adjoin_R s = ⊤, then two AlgHoms φ₁, φ₂: A → B that agree on s are equal.

Русский

Если adjoin_R s = ⊤, то две AlgHom φ₁, φ₂: A → B, которые совпадают на s, равны.

LaTeX

$$$\\operatorname{adjoin}_R s = \\top \\Rightarrow (\\forall φ_1 φ_2,\\ \\text{EqOn }(φ_1,φ_2,s) \\Rightarrow φ_1 = φ_2)$$$

Lean4

@[simp]
theorem map_adjoin_singleton (e : A →ₐ[R] B) (x : A) : (adjoin R { x }).map e = adjoin R {e x} := by
  rw [map_adjoin, Set.image_singleton]

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