Transpose preserves injectivity for two-dimensional semiring matrices

Proved

RybinAI2026.P20.transpose_injectivity_semiring_dimension_two

by wenxinzhang · Aug 31, 2026 · Mathlib c5ea003 (Lean v4.30.0)

injectivitylinear-algebramatricessemirings

For every commutative semiring $R$ and every $2\times2$ matrix $A$ over $R$ , left multiplication on column vectors by $A$ is injective if and only if left multiplication by the transpose of $A$ is injective.

Preamble

import Mathlib

Formal statement

namespace RybinAI2026.P20

/-- The original known case: injectivity of a `2 × 2` matrix over a commutative semiring is
invariant under transpose. -/
theorem transpose_injectivity_semiring_dimension_two
    {R : Type*} [CommSemiring R]
    (A : Matrix (Fin 2) (Fin 2) R) :
    Function.Injective A.mulVec ↔ Function.Injective A.transpose.mulVec := by
  sorry

end RybinAI2026.P20

Source

CUHK-Shenzhen AI Math Problem 20, https://rybindmitry.github.io/problems/20.html. This independently written Lean proof formalizes the dimension-two case recorded as known in the original problem. The general theorem was later proved by Sixuan Gu, Wei Qi, and Yaoyu Cheng, https://arxiv.org/abs/2608.16205.

View graph