doc-next-gen

Mathlib.Algebra.Algebra.Bilinear

Module docstring

{"# 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. "}

LinearMap.mulLeft definition
(a : A) : A →ₗ[R] A
Full source 
/-- The multiplication on the left in a algebra is a linear map.

Note that this only assumes `SMulCommClass R A A`, so that it also works for `R := Aᵐᵒᵖ`.

When `A` is unital and associative, this is the same as `DistribMulAction.toLinearMap R A a` -/
def mulLeft (a : A) : A →ₗ[R] A where
  toFun := (a * ·)
  map_add' := mul_add _
  map_smul' _ := mul_smul_comm _ _
Left multiplication as a linear map
Informal description
For a given element $a$ in an algebra $A$ over a semiring $R$ where scalar multiplication commutes (i.e., $R$ and $A$ satisfy `SMulCommClass R A A`), the left multiplication map $L_a \colon A \to A$ defined by $L_a(b) = a \cdot b$ is a linear map over $R$. When $A$ is unital and associative, this coincides with the linear map induced by the distributive multiplicative action of $R$ on $A$.
LinearMap.mulLeft_apply theorem
(a b : A) : mulLeft R a b = a * b
Full source 
@[simp]
theorem mulLeft_apply (a b : A) : mulLeft R a b = a * b := rfl
Left Multiplication Linear Map Application: $L_a(b) = a \cdot b$
Informal description
For any elements $a$ and $b$ in an algebra $A$ over a semiring $R$, the application of the left multiplication linear map $L_a$ to $b$ equals the product $a \cdot b$ in $A$, i.e., $L_a(b) = a \cdot b$.
LinearMap.mulLeft_toAddMonoidHom theorem
(a : A) : (mulLeft R a : A →+ A) = AddMonoidHom.mulLeft a
Full source 
@[simp]
theorem mulLeft_toAddMonoidHom (a : A) : (mulLeft R a : A →+ A) = AddMonoidHom.mulLeft a := rfl
Equality of Left Multiplication as Additive Monoid Homomorphism and Linear Map
Informal description
For any element $a$ in an algebra $A$ over a semiring $R$, the underlying additive monoid homomorphism of the left multiplication linear map $\text{mulLeft}_R(a) \colon A \to A$ coincides with the additive monoid homomorphism $\text{AddMonoidHom.mulLeft}(a)$ defined by $x \mapsto a \cdot x$.
LinearMap.mulLeft_zero_eq_zero theorem
: mulLeft R (0 : A) = 0
Full source 
@[simp]
theorem mulLeft_zero_eq_zero : mulLeft R (0 : A) = 0 := ext fun _ => zero_mul _
Left Multiplication by Zero Yields the Zero Map
Informal description
For any algebra $A$ over a semiring $R$, the left multiplication linear map associated with the zero element of $A$ is equal to the zero linear map, i.e., $L_0 = 0$.
LinearMap.mulRight definition
(b : A) : A →ₗ[R] A
Full source 
/-- The multiplication on the right in an algebra is a linear map.

Note that this only assumes `IsScalarTower R A A`, so that it also works for `R := A`.

When `A` is unital and associative, this is the same as
`DistribMulAction.toLinearMap R A (MulOpposite.op b)`. -/
def mulRight (b : A) : A →ₗ[R] A where
  toFun := (· * b)
  map_add' _ _ := add_mul _ _ _
  map_smul' _ _ := smul_mul_assoc _ _ _
Right multiplication linear map in an algebra
Informal description
For an algebra \( A \) over a semiring \( R \) and an element \( b \in A \), the right multiplication map \( \text{mulRight}_R(b) \colon A \to A \) is defined by \( x \mapsto x \cdot b \). This map is \( R \)-linear, meaning it satisfies: 1. Additivity: \( \text{mulRight}_R(b)(x + y) = \text{mulRight}_R(b)(x) + \text{mulRight}_R(b)(y) \) for all \( x, y \in A \) 2. Linearity: \( \text{mulRight}_R(b)(r \cdot x) = r \cdot \text{mulRight}_R(b)(x) \) for all \( r \in R \) and \( x \in A \) This construction only requires the scalar multiplication tower property \( \text{IsScalarTower } R A A \), so it also works when \( R = A \).
LinearMap.mulRight_apply theorem
(a b : A) : mulRight R a b = b * a
Full source 
@[simp]
theorem mulRight_apply (a b : A) : mulRight R a b = b * a := rfl
Right multiplication linear map evaluation: $\text{mulRight}_R(a)(b) = b \cdot a$
Informal description
For any elements $a$ and $b$ in an algebra $A$ over a semiring $R$, the right multiplication linear map $\text{mulRight}_R(a)$ evaluated at $b$ equals $b \cdot a$.
LinearMap.mulRight_toAddMonoidHom theorem
(a : A) : (mulRight R a : A →+ A) = AddMonoidHom.mulRight a
Full source 
@[simp]
theorem mulRight_toAddMonoidHom (a : A) : (mulRight R a : A →+ A) = AddMonoidHom.mulRight a := rfl
Right Multiplication Linear Map as Additive Monoid Homomorphism
Informal description
For any element $a$ in an algebra $A$ over a semiring $R$, the right multiplication linear map $\text{mulRight}_R(a) \colon A \to A$ (viewed as an additive monoid homomorphism) coincides with the additive monoid homomorphism $\text{AddMonoidHom.mulRight}(a)$ defined by right multiplication by $a$.
LinearMap.mulRight_zero_eq_zero theorem
: mulRight R (0 : A) = 0
Full source 
@[simp]
theorem mulRight_zero_eq_zero : mulRight R (0 : A) = 0 := ext fun _ => mul_zero _
Right Multiplication by Zero Yields the Zero Map
Informal description
For any algebra $A$ over a semiring $R$, the right multiplication linear map by the zero element is equal to the zero map, i.e., $\text{mulRight}_R(0) = 0$.
LinearMap.mul definition
: A →ₗ[R] A →ₗ[R] A
Full source 
/-- The multiplication in a non-unital non-associative algebra is a bilinear map.

A weaker version of this for semirings exists as `AddMonoidHom.mul`. -/
@[simps!]
def mul : A →ₗ[R] A →ₗ[R] A :=
  LinearMap.mk₂ R (· * ·) add_mul smul_mul_assoc mul_add mul_smul_comm
Bilinear multiplication map in a non-unital non-associative algebra
Informal description
The bilinear map representing the multiplication operation in a non-unital non-associative algebra $A$ over a semiring $R$. Specifically, it maps each pair $(x, y) \in A \times A$ to their product $x \cdot y \in A$, and satisfies the following properties: 1. Additivity in the first argument: $(x_1 + x_2) \cdot y = x_1 \cdot y + x_2 \cdot y$ for all $x_1, x_2, y \in A$ 2. Linearity in the first argument: $(r \cdot x) \cdot y = r \cdot (x \cdot y)$ for all $r \in R$ and $x, y \in A$ 3. Additivity in the second argument: $x \cdot (y_1 + y_2) = x \cdot y_1 + x \cdot y_2$ for all $x, y_1, y_2 \in A$ 4. Linearity in the second argument: $x \cdot (r \cdot y) = r \cdot (x \cdot y)$ for all $r \in R$ and $x, y \in A$
LinearMap.mul' definition
: A ⊗[R] A →ₗ[R] A
Full source 
/-- The multiplication map on a non-unital algebra, as an `R`-linear map from `A ⊗[R] A` to `A`. -/
-- TODO: upgrade to A-linear map if A is a semiring.
noncomputable def mul' : A ⊗[R] AA ⊗[R] A →ₗ[R] A :=
  TensorProduct.lift (mul R A)
Multiplication map on a non-unital algebra as a linear map from the tensor product
Informal description
The linear map representing the multiplication operation in a non-unital algebra $A$ over a semiring $R$, defined on the tensor product $A \otimes_R A$ and mapping to $A$. Specifically, it sends a tensor $x \otimes y$ to the product $x \cdot y$ in $A$.
LinearMap.mulLeftRight definition
(ab : A × A) : A →ₗ[R] A
Full source 
/-- Simultaneous multiplication on the left and right is a linear map. -/
def mulLeftRight (ab : A × A) : A →ₗ[R] A :=
  (mulRight R ab.snd).comp (mulLeft R ab.fst)
Simultaneous left and right multiplication as a linear map
Informal description
For an algebra \( A \) over a commutative semiring \( R \) and a pair of elements \( (a, b) \in A \times A \), the linear map \( \text{mulLeftRight}_R(a, b) \colon A \to A \) is defined by \( x \mapsto a \cdot x \cdot b \). This map is constructed as the composition of the left multiplication by \( a \) and the right multiplication by \( b \), both of which are \( R \)-linear maps.
LinearMap.mul_apply' theorem
(a b : A) : mul R A a b = a * b
Full source 
@[simp]
theorem mul_apply' (a b : A) : mul R A a b = a * b :=
  rfl
Evaluation of bilinear multiplication map: $\text{mul}_R(a, b) = a \cdot b$
Informal description
For any elements $a, b$ in a non-unital non-associative algebra $A$ over a semiring $R$, the bilinear multiplication map $\text{mul}_R(a, b)$ evaluates to the product $a \cdot b$.
LinearMap.mulLeftRight_apply theorem
(a b x : A) : mulLeftRight R (a, b) x = a * x * b
Full source 
@[simp]
theorem mulLeftRight_apply (a b x : A) : mulLeftRight R (a, b) x = a * x * b :=
  rfl
Evaluation of Simultaneous Left and Right Multiplication Map: $\text{mulLeftRight}_R(a, b)(x) = a \cdot x \cdot b$
Informal description
For any elements $a, b, x$ in an algebra $A$ over a commutative semiring $R$, the linear map $\text{mulLeftRight}_R(a, b)$ evaluated at $x$ satisfies $\text{mulLeftRight}_R(a, b)(x) = a \cdot x \cdot b$.
LinearMap.mul'_apply theorem
{a b : A} : mul' R A (a ⊗ₜ b) = a * b
Full source 
@[simp]
theorem mul'_apply {a b : A} : mul' R A (a ⊗ₜ b) = a * b :=
  rfl
Evaluation of Tensor Product Multiplication Map: $\text{mul}'_R(a \otimes b) = a \cdot b$
Informal description
For any elements $a, b$ in a non-unital non-associative algebra $A$ over a semiring $R$, the linear map $\text{mul}'_R$ evaluated at the tensor product $a \otimes b$ equals the product $a \cdot b$ in $A$, i.e., $\text{mul}'_R(a \otimes b) = a \cdot b$.
LinearMap.mulLeft_mul theorem
[SMulCommClass R A A] (a b : A) : mulLeft R (a * b) = (mulLeft R a).comp (mulLeft R b)
Full source 
@[simp]
theorem mulLeft_mul [SMulCommClass R A A] (a b : A) :
    mulLeft R (a * b) = (mulLeft R a).comp (mulLeft R b) := by
  ext
  simp only [mulLeft_apply, comp_apply, mul_assoc]
Composition of Left Multiplication Maps in an Algebra
Informal description
Let $A$ be an algebra over a semiring $R$ such that the scalar multiplications by $R$ and $A$ on $A$ commute. For any elements $a, b \in A$, the left multiplication map $L_{a \cdot b} \colon A \to A$ defined by $x \mapsto (a \cdot b) \cdot x$ is equal to the composition $L_a \circ L_b$ of the left multiplication maps $L_a$ and $L_b$.
LinearMap.mulRight_mul theorem
[IsScalarTower R A A] (a b : A) : mulRight R (a * b) = (mulRight R b).comp (mulRight R a)
Full source 
@[simp]
theorem mulRight_mul [IsScalarTower R A A] (a b : A) :
    mulRight R (a * b) = (mulRight R b).comp (mulRight R a) := by
  ext
  simp only [mulRight_apply, comp_apply, mul_assoc]
Composition of Right Multiplication Maps in an Algebra
Informal description
Let $A$ be an algebra over a semiring $R$ such that the scalar multiplication satisfies the tower property $\text{IsScalarTower } R A A$. For any elements $a, b \in A$, the right multiplication linear map $\text{mulRight}_R(a \cdot b)$ is equal to the composition of the right multiplication linear maps $\text{mulRight}_R(b) \circ \text{mulRight}_R(a)$.
NonUnitalAlgHom.lmul definition
: A →ₙₐ[R] End R A
Full source 
/-- 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`. -/
def _root_.NonUnitalAlgHom.lmul : A →ₙₐ[R] End R A where
  __ := mul R A
  map_mul' := mulLeft_mul _ _
  map_zero' := mulLeft_zero_eq_zero _ _
Left multiplication as a non-unital algebra homomorphism
Informal description
The left multiplication map in a non-unital algebra $A$ over a semiring $R$ is a non-unital algebra homomorphism from $A$ to the endomorphism ring $\text{End}_R(A)$. Specifically, for each $a \in A$, the map $\text{lmul}(a) \colon A \to A$ is defined by $x \mapsto a \cdot x$, and the assignment $a \mapsto \text{lmul}(a)$ preserves the multiplication structure.
NonUnitalAlgHom.coe_lmul_eq_mul theorem
: ⇑(NonUnitalAlgHom.lmul R A) = mul R A
Full source 
@[simp]
theorem _root_.NonUnitalAlgHom.coe_lmul_eq_mul : ⇑(NonUnitalAlgHom.lmul R A) = mul R A :=
  rfl
Equality of Left Multiplication Homomorphism and Bilinear Multiplication Map
Informal description
The underlying function of the left multiplication non-unital algebra homomorphism $\text{lmul} \colon A \to \text{End}_R(A)$ in a non-unital algebra $A$ over a semiring $R$ coincides with the bilinear multiplication map $\text{mul} \colon A \to A \to A$.
LinearMap.commute_mulLeft_right theorem
(a b : A) : Commute (mulLeft R a) (mulRight R b)
Full source 
theorem commute_mulLeft_right (a b : A) : Commute (mulLeft R a) (mulRight R b) := by
  ext c
  exact (mul_assoc a c b).symm
Commutativity of Left and Right Multiplication Maps in an Algebra
Informal description
For any elements $a$ and $b$ in an algebra $A$ over a semiring $R$, the left multiplication map $L_a$ and the right multiplication map $R_b$ commute, i.e., $L_a \circ R_b = R_b \circ L_a$.
LinearMap.map_mul_iff theorem
(f : A →ₗ[R] B) : (∀ x y, f (x * y) = f x * f y) ↔ (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f
Full source 
/-- A `LinearMap` preserves multiplication if pre- and post- composition with `LinearMap.mul` are
equivalent. By converting the statement into an equality of `LinearMap`s, this lemma allows various
specialized `ext` lemmas about `→ₗ[R]` to then be applied.

This is the `LinearMap` version of `AddMonoidHom.map_mul_iff`. -/
theorem map_mul_iff (f : A →ₗ[R] B) :
    (∀ x y, f (x * y) = f x * f y) ↔
      (LinearMap.mul R A).compr₂ f = (LinearMap.mul R B ∘ₗ f).compl₂ f :=
  Iff.symm LinearMap.ext_iff₂
Characterization of Multiplicative Linear Maps via Bilinear Diagram Commutativity
Informal description
Let $A$ and $B$ be non-unital non-associative algebras over a commutative semiring $R$, and let $f : A \to B$ be an $R$-linear map. Then $f$ preserves multiplication (i.e., $f(x * y) = f(x) * f(y)$ for all $x, y \in A$) if and only if the following diagram commutes: $$ \begin{CD} A \otimes_R A @>{f \otimes f}>> B \otimes_R B \\ @V{\text{mul}_A}VV @VV{\text{mul}_B}V \\ A @>{f}>> B \end{CD} $$ where $\text{mul}_A$ and $\text{mul}_B$ denote the multiplication operations in $A$ and $B$ respectively, viewed as $R$-bilinear maps.
LinearMap.mulLeft_one theorem
: mulLeft R (1 : A) = LinearMap.id
Full source 
@[simp]
theorem mulLeft_one : mulLeft R (1 : A) = LinearMap.id := ext fun _ => one_mul _
Left Multiplication by One is the Identity Map
Informal description
For any algebra $A$ over a semiring $R$ where scalar multiplication commutes, the left multiplication map by the multiplicative identity $1 \in A$ is equal to the identity linear map on $A$, i.e., $L_1 = \text{id}_A$.
LinearMap.mulLeft_eq_zero_iff theorem
(a : A) : mulLeft R a = 0 ↔ a = 0
Full source 
@[simp]
theorem mulLeft_eq_zero_iff (a : A) : mulLeftmulLeft R a = 0 ↔ a = 0 := by
  constructor <;> intro h
  · rw [← mul_one a, ← mulLeft_apply R a 1, h, LinearMap.zero_apply]
  · rw [h]
    exact mulLeft_zero_eq_zero _ _
Left Multiplication by Zero Characterization: $L_a = 0 \leftrightarrow a = 0$
Informal description
For any element $a$ in an algebra $A$ over a semiring $R$, the left multiplication linear map $L_a$ is equal to the zero map if and only if $a = 0$.
LinearMap.pow_mulLeft theorem
(a : A) (n : ℕ) : mulLeft R a ^ n = mulLeft R (a ^ n)
Full source 
@[simp]
theorem pow_mulLeft (a : A) (n : ℕ) : mulLeft R a ^ n = mulLeft R (a ^ n) :=
  match n with
  | 0 => by rw [pow_zero, pow_zero, mulLeft_one, Module.End.one_eq_id]
  | (n + 1) => by rw [pow_succ, pow_succ, mulLeft_mul, Module.End.mul_eq_comp, pow_mulLeft]
Power of Left Multiplication Map in an Algebra: $(L_a)^n = L_{a^n}$
Informal description
Let $A$ be an algebra over a semiring $R$ with commuting scalar multiplication. For any element $a \in A$ and natural number $n$, the $n$-th power of the left multiplication map $L_a$ is equal to the left multiplication map by $a^n$, i.e., $(L_a)^n = L_{a^n}$.
LinearMap.mulRight_one theorem
: mulRight R (1 : A) = LinearMap.id
Full source 
@[simp]
theorem mulRight_one : mulRight R (1 : A) = LinearMap.id := ext fun _ => mul_one _
Right Multiplication by One is the Identity Map
Informal description
For an algebra $A$ over a semiring $R$, the right multiplication linear map by the multiplicative identity $1 \in A$ is equal to the identity linear map on $A$.
LinearMap.mulRight_eq_zero_iff theorem
(a : A) : mulRight R a = 0 ↔ a = 0
Full source 
@[simp]
theorem mulRight_eq_zero_iff (a : A) : mulRightmulRight R a = 0 ↔ a = 0 := by
  constructor <;> intro h
  · rw [← one_mul a, ← mulRight_apply R a 1, h, LinearMap.zero_apply]
  · rw [h]
    exact mulRight_zero_eq_zero _ _
Right Multiplication by Zero is the Zero Map: $\text{mulRight}_R(a) = 0 \leftrightarrow a = 0$
Informal description
For any element $a$ in an algebra $A$ over a semiring $R$, the right multiplication linear map $\text{mulRight}_R(a)$ is equal to the zero map if and only if $a = 0$.
LinearMap.pow_mulRight theorem
(a : A) (n : ℕ) : mulRight R a ^ n = mulRight R (a ^ n)
Full source 
@[simp]
theorem pow_mulRight (a : A) (n : ℕ) : mulRight R a ^ n = mulRight R (a ^ n) :=
  match n with
  | 0 => by rw [pow_zero, pow_zero, mulRight_one, Module.End.one_eq_id]
  | (n + 1) => by rw [pow_succ, pow_succ', mulRight_mul, Module.End.mul_eq_comp, pow_mulRight]
Power of Right Multiplication Map Equals Right Multiplication of Power: $(\text{mulRight}_R(a))^n = \text{mulRight}_R(a^n)$
Informal description
For any element $a$ in an algebra $A$ over a semiring $R$ and any natural number $n$, the $n$-th power of the right multiplication linear map $\text{mulRight}_R(a)$ is equal to the right multiplication linear map of the $n$-th power of $a$, i.e., $(\text{mulRight}_R(a))^n = \text{mulRight}_R(a^n)$.
Algebra.lmul definition
: A →ₐ[R] End R A
Full source 
/-- 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.lmul`. -/
def _root_.Algebra.lmul : A →ₐ[R] End R A where
  __ := NonUnitalAlgHom.lmul R A
  map_one' := mulLeft_one _ _
  commutes' r := ext fun a => (Algebra.smul_def r a).symm
Algebra multiplication as an algebra homomorphism to endomorphisms
Informal description
The multiplication operation in an algebra $A$ over a semiring $R$ can be viewed as an algebra homomorphism from $A$ to the ring of $R$-linear endomorphisms of $A$. Specifically, for each $a \in A$, the map $\text{lmul}(a) \colon A \to A$ is defined by $x \mapsto a \cdot x$, and the assignment $a \mapsto \text{lmul}(a)$ preserves the algebra structure, including the multiplicative identity and scalar multiplication.
Algebra.coe_lmul_eq_mul theorem
: ⇑(Algebra.lmul R A) = mul R A
Full source 
@[simp]
theorem _root_.Algebra.coe_lmul_eq_mul : ⇑(Algebra.lmul R A) = mul R A :=
  rfl
Equality of Left Multiplication Map and Algebra Multiplication Function
Informal description
The underlying function of the algebra left multiplication map $\text{lmul}_{R,A} \colon A \to \text{End}_R(A)$ is equal to the multiplication map $\text{mul}_{R,A} \colon A \to A \to A$ in the algebra $A$ over the semiring $R$.
Algebra.lmul_injective theorem
: Function.Injective (Algebra.lmul R A)
Full source 
theorem _root_.Algebra.lmul_injective : Function.Injective (Algebra.lmul R A) :=
  fun a₁ a₂ h ↦ by simpa using DFunLike.congr_fun h 1
Injectivity of Left Multiplication in $R$-Algebras
Informal description
For any commutative semiring $R$ and $R$-algebra $A$, the algebra homomorphism $\text{lmul} \colon A \to \text{End}_R(A)$ defined by left multiplication is injective. That is, if $\text{lmul}(a) = \text{lmul}(b)$ for some $a, b \in A$, then $a = b$.
Algebra.lmul_isUnit_iff theorem
{x : A} : IsUnit (Algebra.lmul R A x) ↔ IsUnit x
Full source 
theorem _root_.Algebra.lmul_isUnit_iff {x : A} :
    IsUnitIsUnit (Algebra.lmul R A x) ↔ IsUnit x := by
  rw [Module.End.isUnit_iff, Iff.comm]
  exact IsUnit.isUnit_iff_mulLeft_bijective
Characterization of units in an algebra via bijective left multiplication
Informal description
Let $A$ be an algebra over a commutative semiring $R$. For any element $x \in A$, the left multiplication map $L_x : A \to A$ defined by $L_x(y) = x \cdot y$ is a unit in the endomorphism ring $\text{End}_R(A)$ if and only if $x$ is a unit in $A$.
LinearMap.toSpanSingleton_eq_algebra_linearMap theorem
: toSpanSingleton R A 1 = Algebra.linearMap R A
Full source 
theorem toSpanSingleton_eq_algebra_linearMap : toSpanSingleton R A 1 = Algebra.linearMap R A := by
  ext; simp
Equality of Unit Span Map and Algebra Linear Map
Informal description
Let $R$ be a commutative semiring and $A$ be an $R$-algebra. The linear map $\text{toSpanSingleton}_R^A(1)$ from $R$ to $A$, which sends $r \in R$ to $r \cdot 1_A$, is equal to the canonical algebra linear map $\text{Algebra.linearMap}_R^A$ from $R$ to $A$.
LinearMap.mulLeft_injective theorem
[NoZeroDivisors A] {x : A} (hx : x ≠ 0) : Function.Injective (mulLeft R x)
Full source 
@[deprecated mul_right_injective₀ (since := "2024-11-18")]
theorem mulLeft_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :
    Function.Injective (mulLeft R x) :=
  mul_right_injective₀ hx
Injectivity of Left Multiplication by Nonzero Elements in Algebras without Zero Divisors
Informal description
Let $A$ be an algebra over a commutative semiring $R$ with no zero divisors. For any nonzero element $x \in A$, the left multiplication map $L_x \colon A \to A$ defined by $L_x(y) = x \cdot y$ is injective.
LinearMap.mulRight_injective theorem
[NoZeroDivisors A] {x : A} (hx : x ≠ 0) : Function.Injective (mulRight R x)
Full source 
@[deprecated mul_left_injective₀ (since := "2024-11-18")]
theorem mulRight_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) :
    Function.Injective (mulRight R x) :=
  mul_left_injective₀ hx
Injectivity of Right Multiplication by Nonzero Elements in Algebras without Zero Divisors
Informal description
Let $A$ be an algebra over a commutative semiring $R$ with no zero divisors. For any nonzero element $x \in A$, the right multiplication map $A \to A$ defined by $y \mapsto y \cdot x$ is injective.
LinearMap.mul_injective theorem
[NoZeroDivisors A] {x : A} (hx : x ≠ 0) : Function.Injective (mul R A x)
Full source 
@[deprecated mul_right_injective₀ (since := "2024-11-18")]
theorem mul_injective [NoZeroDivisors A] {x : A} (hx : x ≠ 0) : Function.Injective (mul R A x) :=
   mul_right_injective₀ hx
Injectivity of Multiplication by Nonzero Elements in Algebras without Zero Divisors
Informal description
Let $A$ be an algebra over a commutative semiring $R$ with no zero divisors. For any nonzero element $x \in A$, the multiplication map $A \to A$ defined by $y \mapsto x \cdot y$ is injective.