of_injective — Mathlib

English

If R is nontrivial and M has an AddZeroClass structure, the embedding of AddMonoidAlgebra R M is injective and hence identifies AddMonoidAlgebra inside MonoidAlgebra.

Русский

Если R ненулевое и M имеет AddZeroClass, отображение of R M инъективно и тем самым идентифицирует AddMonoidAlgebra внутри MonoidAlgebra.

LaTeX

$$$\\mathrm{of\\_injective}\\ R\\ M$.$$

Lean4

theorem of_injective [Nontrivial R] [AddZeroClass M] : Function.Injective (of R M) :=
  MonoidAlgebra.of_injective

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