linear_map.mul'' #
this defines the multiplication map $M_{n\times n} \to M_n$
theorem
commutes_with_unit_iff
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(f : A →ₗ[R] B) :
f.comp (algebra.linear_map R A) = algebra.linear_map R B ↔ ⇑f 1 = 1
theorem
matrix.kronecker_product.ext_iff
{R : Type u_1}
{P : Type u_2}
{n₁ : Type u_3}
{n₂ : Type u_4}
[fintype n₁]
[fintype n₂]
[comm_semiring R]
[add_comm_monoid P]
[module R P]
[decidable_eq n₁]
[decidable_eq n₂]
{g h : matrix (n₁ × n₂) (n₁ × n₂) R →ₗ[R] P} :
g = h ↔ ∀ (x : matrix n₁ n₁ R) (y : matrix n₂ n₂ R), ⇑g (matrix.kronecker_map has_mul.mul x y) = ⇑h (matrix.kronecker_map has_mul.mul x y)
def
linear_map.mul_to_clm
(𝕜 : Type u_1)
(X : Type (max u_2 u_3))
[is_R_or_C 𝕜]
[normed_add_comm_group_of_ring X]
[normed_space 𝕜 X]
[smul_comm_class 𝕜 X X]
[is_scalar_tower 𝕜 X X]
[finite_dimensional 𝕜 X] :
Equations
- linear_map.mul_to_clm 𝕜 X = {to_linear_map := {to_fun := ⇑(mul_map_aux 𝕜 X), map_add' := _, map_smul' := _}, cont := _}
theorem
linear_map.mul_to_clm_apply
{𝕜 : Type u_1}
{X : Type (max u_2 u_3)}
[is_R_or_C 𝕜]
[normed_add_comm_group_of_ring X]
[normed_space 𝕜 X]
[smul_comm_class 𝕜 X X]
[is_scalar_tower 𝕜 X X]
[finite_dimensional 𝕜 X]
(x y : X) :
⇑(⇑(linear_map.mul_to_clm 𝕜 X) x) y = x * y