lmul_injective — Mathlib

English

For any commutative semiring R and algebra A over R, the map a ↦ (x ↦ a x) from A to End_R(A) is injective; i.e., if a_1 x = a_2 x for all x ∈ A, then a_1 = a_2.

Русский

Для любой пары R и A, где R — коммутативное полукольцо, отображение a ↦ (x ↦ a x) из A в End_R(A) инъективно; если a_1 x = a_2 x для всех x, значит a_1 = a_2.

LaTeX

$$$\forall a_1,a_2\in A:\ (\forall x\in A:\ a_1 x = a_2 x) \Rightarrow a_1=a_2.$$$

Lean4

theorem _root_.Algebra.lmul_injective : Function.Injective (Algebra.lmul R A) := fun a₁ a₂ h ↦ by
  simpa using DFunLike.congr_fun h 1

Похожие утверждения