leftMulMatrix_injective — Mathlib

English

Reiterating: the map x ↦ leftMulMatrix b x is injective.

Русский

Повторно: отображение x ↦ leftMulMatrix b x инъективно.

LaTeX

$$$\text{Injective}(\operatorname{leftMulMatrix}\; b).$$$

Lean4

theorem leftMulMatrix_injective : Function.Injective (leftMulMatrix b) := fun x x' h ↦
  calc
    x = Algebra.lmul R S x 1 := (mul_one x).symm
    _ = Algebra.lmul R S x' 1 := by rw [(LinearMap.toMatrix b b).injective h]
    _ = x' := mul_one x'

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