linear_map.mul''

this defines the multiplication map $M_{n\times n} \to M_n$

theorem commutes_with_unit_iff {R : Type u_3} {A : Type u_1} {B : Type u_2} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₗ[R] B) : f ∘ₗ Algebra.linearMap R A = Algebra.linearMap R B ↔ f 1 = 1

theorem commutes_with_mul'_iff {R : Type u_2} {A : Type u_1} {B : Type u_3} [CommSemiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [IsScalarTower R A A] [NonUnitalNonAssocSemiring B] [Module R B] [SMulCommClass R B B] [IsScalarTower R B B] (f : A →ₗ[R] B) : LinearMap.mul' R B ∘ₗ TensorProduct.map f f = f ∘ₗ LinearMap.mul' R A ↔ ∀ (x y : A), f (x * y) = f x * f y

theorem LinearMap.adjoint_commutes_with_mul_adjoint_iff {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [RCLike 𝕜] [NormedAddCommGroupOfRing X] [NormedAddCommGroupOfRing Y] [InnerProductSpace 𝕜 X] [InnerProductSpace 𝕜 Y] [SMulCommClass 𝕜 X X] [SMulCommClass 𝕜 Y Y] [IsScalarTower 𝕜 X X] [IsScalarTower 𝕜 Y Y] [FiniteDimensional 𝕜 X] [FiniteDimensional 𝕜 Y] (f : X →ₗ[𝕜] Y) : TensorProduct.map (LinearMap.adjoint f) (LinearMap.adjoint f) ∘ₗ LinearMap.adjoint (LinearMap.mul' 𝕜 Y) = LinearMap.adjoint (LinearMap.mul' 𝕜 X) ∘ₗ LinearMap.adjoint f ↔ ∀ (x y : X), f (x * y) = f x * f y

theorem LinearMap.commutes_with_mul_adjoint_iff {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [RCLike 𝕜] [NormedAddCommGroupOfRing X] [NormedAddCommGroupOfRing Y] [InnerProductSpace 𝕜 X] [InnerProductSpace 𝕜 Y] [SMulCommClass 𝕜 X X] [SMulCommClass 𝕜 Y Y] [IsScalarTower 𝕜 X X] [IsScalarTower 𝕜 Y Y] [FiniteDimensional 𝕜 X] [FiniteDimensional 𝕜 Y] (f : X →ₗ[𝕜] Y) : TensorProduct.map f f ∘ₗ LinearMap.adjoint (LinearMap.mul' 𝕜 X) = LinearMap.adjoint (LinearMap.mul' 𝕜 Y) ∘ₗ f ↔ ∀ (x y : Y), (LinearMap.adjoint f) (x * y) = (LinearMap.adjoint f) x * (LinearMap.adjoint f) y

theorem LinearIsometryEquiv.commutes_with_mul_adjoint_iff_of_surjective_isometry {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [RCLike 𝕜] [NormedAddCommGroupOfRing X] [NormedAddCommGroupOfRing Y] [InnerProductSpace 𝕜 X] [InnerProductSpace 𝕜 Y] [SMulCommClass 𝕜 X X] [SMulCommClass 𝕜 Y Y] [IsScalarTower 𝕜 X X] [IsScalarTower 𝕜 Y Y] [FiniteDimensional 𝕜 X] [FiniteDimensional 𝕜 Y] (f : X ≃ₗᵢ[𝕜] Y) : TensorProduct.map ↑f.toLinearEquiv ↑f.toLinearEquiv ∘ₗ LinearMap.adjoint (LinearMap.mul' 𝕜 X) = LinearMap.adjoint (LinearMap.mul' 𝕜 Y) ∘ₗ ↑f.toLinearEquiv ↔ ∀ (x y : X), f (x * y) = f x * f y

theorem Matrix.KroneckerProduct.ext_iff {R : Type u_1} {P : Type u_2} {n₁ : Type u_3} {n₂ : Type u_4} [Fintype n₁] [Fintype n₂] [CommSemiring R] [AddCommMonoid P] [Module R P] [DecidableEq n₁] [DecidableEq n₂] {g : Matrix (n₁ × n₂) (n₁ × n₂) R →ₗ[R] P} {h : Matrix (n₁ × n₂) (n₁ × n₂) R →ₗ[R] P} : g = h ↔ ∀ (x : Matrix n₁ n₁ R) (y : Matrix n₂ n₂ R), g (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y) = h (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y)

def LinearMap.mulToClm (𝕜 : Type u_1) (X : Type u_2) [RCLike 𝕜] [NormedAddCommGroupOfRing X] [NormedSpace 𝕜 X] [SMulCommClass 𝕜 X X] [IsScalarTower 𝕜 X X] [FiniteDimensional 𝕜 X] : X →L[𝕜] X →L[𝕜] X

Equations

• LinearMap.mulToClm 𝕜 X = { toFun := ⇑(mul_map_aux 𝕜 X), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

theorem LinearMap.mulToClm_apply {𝕜 : Type u_1} {X : Type u_2} [RCLike 𝕜] [NormedAddCommGroupOfRing X] [NormedSpace 𝕜 X] [SMulCommClass 𝕜 X X] [IsScalarTower 𝕜 X X] [FiniteDimensional 𝕜 X] (x : X) (y : X) : ((LinearMap.mulToClm 𝕜 X) x) y = x * y