instIsFaithfulMatrixForall — Mathlib

English

The natural action of matrices on the standard module is faithful; the map sending a matrix to its action on R^n is injective.

Русский

Естественное действие матриц на стандартном модуле безусловно верно; отображение матрицы в её действие инъективно.

LaTeX

$$IsFaithful_R(Matrix n n R) (n → R)$$

Lean4

instance : IsFaithful R (Matrix n n R) (n → R) where injective_toEnd := by simpa using EmbeddingLike.injective _

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