vecMul_injective_iff_isUnit — Mathlib

English

For A, vecMul is injective if and only if A is a unit.

Русский

Для матрицы A инъективность vecMul эквивалентна тому, что A — единица.

LaTeX

$$Injective A.vecMul ↔ IsUnit A$$

Lean4

theorem vecMul_injective_iff_isUnit {A : Matrix m m K} : Function.Injective A.vecMul ↔ IsUnit A :=
  by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← vecMul_surjective_iff_isUnit]
    exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h
  change Function.Injective A.vecMulLinear
  rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
  intro c hc
  replace h := h.invertible
  simpa using congr_arg A⁻¹.vecMulLinear hc

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