transpose_eq_ofNat — Mathlib

English

For any natural d and matrix M, M^T = OfNat.ofNat(d) if and only if M = OfNat.ofNat(d).

Русский

Для любого натурального d и матрицы M верно: M^T = OfNat.ofNat(d) тогда и только тогда, когда M = OfNat.ofNat(d).

LaTeX

$$$M^{\top} = \mathrm{OfNat.ofNat}(d) \iff M = \mathrm{OfNat.ofNat}(d)$$$

Lean4

@[simp]
theorem transpose_eq_ofNat [DecidableEq n] [AddMonoidWithOne α] {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] :
    Mᵀ = ofNat(d) ↔ M = OfNat.ofNat d :=
  transpose_eq_diagonal

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