# Documentation

Mathlib.Algebra.Algebra.Bilinear

# Facts about algebras involving bilinear maps and tensor products #

We move a few basic statements about algebras out of Algebra.Algebra.Basic, in order to avoid importing LinearAlgebra.BilinearMap and LinearAlgebra.TensorProduct unnecessarily.

def LinearMap.mul (R : Type u_1) (A : Type u_2) [] [Module R A] [] [] :

The multiplication in a non-unital non-associative algebra is a bilinear map.

A weaker version of this for semirings exists as AddMonoidHom.mul.

Instances For
def LinearMap.mul' (R : Type u_1) (A : Type u_2) [] [Module R A] [] [] :

The multiplication map on a non-unital algebra, as an R-linear map from A ⊗[R] A to A.

Instances For
def LinearMap.mulLeft (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (a : A) :

The multiplication on the left in a non-unital algebra is a linear map.

Instances For
def LinearMap.mulRight (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (a : A) :

The multiplication on the right in an algebra is a linear map.

Instances For
def LinearMap.mulLeftRight (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (ab : A × A) :

Simultaneous multiplication on the left and right is a linear map.

Instances For
@[simp]
theorem LinearMap.mulLeft_toAddMonoidHom (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (a : A) :
@[simp]
theorem LinearMap.mulRight_toAddMonoidHom (R : Type u_1) {A : Type u_2} [] [Module R A] [] [] (a : A) :
@[simp]
theorem LinearMap.mul_apply' {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
↑(↑() a) b = a * b
@[simp]
theorem LinearMap.mulLeft_apply {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
↑() b = a * b
@[simp]
theorem LinearMap.mulRight_apply {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
↑() b = b * a
@[simp]
theorem LinearMap.mulLeftRight_apply {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) (x : A) :
↑(LinearMap.mulLeftRight R (a, b)) x = a * x * b
@[simp]
theorem LinearMap.mul'_apply {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] {a : A} {b : A} :
↑() (a ⊗ₜ[R] b) = a * b
@[simp]
theorem LinearMap.mulLeft_zero_eq_zero {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
= 0
@[simp]
theorem LinearMap.mulRight_zero_eq_zero {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
= 0
def NonUnitalAlgHom.lmul (R : Type u_1) (A : Type u_2) [] [Module R A] [] [] :

The multiplication in a non-unital algebra is a bilinear map.

A weaker version of this for non-unital non-associative algebras exists as LinearMap.mul.

Instances For
@[simp]
theorem NonUnitalAlgHom.coe_lmul_eq_mul {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] :
↑() = ↑()
theorem LinearMap.commute_mulLeft_right {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
Commute () ()
@[simp]
theorem LinearMap.mulLeft_mul {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
@[simp]
theorem LinearMap.mulRight_mul {R : Type u_1} {A : Type u_2} [] [Module R A] [] [] (a : A) (b : A) :
def Algebra.lmul (R : Type u_1) (A : Type u_2) [] [] [Algebra R A] :

The multiplication in an algebra is an algebra homomorphism into the endomorphisms on the algebra.

A weaker version of this for non-unital algebras exists as NonUnitalAlgHom.mul.

Instances For
@[simp]
theorem Algebra.coe_lmul_eq_mul {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :
↑() = ↑()
@[simp]
theorem LinearMap.mulLeft_eq_zero_iff {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (a : A) :
= 0 a = 0
@[simp]
theorem LinearMap.mulRight_eq_zero_iff {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (a : A) :
= 0 a = 0
@[simp]
theorem LinearMap.mulLeft_one {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :
= LinearMap.id
@[simp]
theorem LinearMap.mulRight_one {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] :
= LinearMap.id
@[simp]
theorem LinearMap.pow_mulLeft {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (a : A) (n : ) :
^ n = LinearMap.mulLeft R (a ^ n)
@[simp]
theorem LinearMap.pow_mulRight {R : Type u_1} {A : Type u_2} [] [] [Algebra R A] (a : A) (n : ) :
^ n = LinearMap.mulRight R (a ^ n)
theorem LinearMap.mulLeft_injective {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] [] {x : A} (hx : x 0) :
theorem LinearMap.mulRight_injective {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] [] {x : A} (hx : x 0) :
theorem LinearMap.mul_injective {R : Type u_1} {A : Type u_2} [] [Ring A] [Algebra R A] [] {x : A} (hx : x 0) :
Function.Injective ↑(↑() x)