single_eq_of_single_single — Mathlib

English

Transpose acts as an algebra isomorphism between matrix algebra and its opposite algebra.

Русский

Транспонирование является алгебраическим изоморфизмом между алгеброй матриц и её противоположной алгеброй.

LaTeX

$$$\mathrm{transposeAlgEquiv} : \mathrm{Mat}_{m\times m}(\alpha) \simeq_\mathsf{Alg} R (\mathrm{Mat}_{m\times m}(\alpha))^{\mathrm{op}}$ is an AlgEquiv.$$

Lean4

/-- See also `single_eq_updateRow_zero` and `single_eq_updateCol_zero`. -/
theorem single_eq_of_single_single (i : m) (j : n) (a : α) : single i j a = Matrix.of (Pi.single i (Pi.single j a)) :=
  by
  ext a b
  unfold single
  by_cases hi : i = a <;> by_cases hj : j = b <;> simp [*]

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