English
The map sending an element x to the matrix of left multiplication by x is injective: different x give different matrices.
Русский
Отображение, отправляющее x в матрицу левого умножения на x, инъективно: разные x дают разные матрицы.
LaTeX
$$$\text{Injective}(\operatorname{leftMulMatrix}\; b).$$$
Lean4
/-- `leftMulMatrix b x` is the matrix corresponding to the linear map `fun y ↦ x * y`.
`leftMulMatrix_eq_repr_mul` gives a formula for the entries of `leftMulMatrix`.
This definition is useful for doing (more) explicit computations with `LinearMap.mulLeft`,
such as the trace form or norm map for algebras.
-/
noncomputable def leftMulMatrix : S →ₐ[R] Matrix m m R
where
toFun x := LinearMap.toMatrix b b (Algebra.lmul R S x)
map_zero' := by rw [map_zero, LinearEquiv.map_zero]
map_one' := by rw [map_one, LinearMap.toMatrix_one]
map_add' x y := by rw [map_add, LinearEquiv.map_add]
map_mul' x y := by rw [map_mul, LinearMap.toMatrix_mul]
commutes'
r := by
ext
rw [lmul_algebraMap, toMatrix_lsmul, algebraMap_eq_diagonal, Pi.algebraMap_def, Algebra.algebraMap_self_apply]
