of_injective — Mathlib

English

If two ring homomorphisms from MonoidAlgebra R M to S agree on singleOneRingHom and on the embedding of MonoidAlgebra.of, they agree on all of MonoidAlgebra.

Русский

Если два кольцевых гомоморфизма из MonoidAlgebra R M в S совпадают на singleOneRingHom и на вложении MonoidAlgebra.of, они совпадают на всём MonoidAlgebra.

LaTeX

$$$ f = g \;\text{if}\; f \circ \operatorname{singleOneRingHom} = g \circ \operatorname{singleOneRingHom}$ и $(f|_{\operatorname{of}}) = (g|_{\operatorname{of}})$$$

Lean4

theorem of_injective [Nontrivial R] : Function.Injective (of R M) := fun a b h ↦ by
  simpa using (single_eq_single_iff _ _ _ _).mp h

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