injective_comp_algebraMap — Mathlib

English

The map sending f to f ∘ algebraMap A K is injective on RingHom K L; i.e., if f1 ∘ algebraMap = f2 ∘ algebraMap, then f1 = f2.

Русский

Отображение, отправляющее f на f ∘ algebraMap A K, инъективно на RingHom K L: если f1 ∘ algebraMap = f2 ∘ algebraMap, то f1 = f2.

LaTeX

$$$\text{Injective } (\lambda f : K \to+* L, f \circ \operatorname{algebraMap} A K)$$$

Lean4

theorem injective_comp_algebraMap : Function.Injective fun (f : K →+* L) => f.comp (algebraMap A K) := fun _ _ h =>
  ringHom_ext (fun x => RingHom.congr_fun h x)

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