conjTranspose_eq_ofNat — Mathlib

English

For any M and d with at least two, M^H = OfNat(d) iff M = OfNat(d).

Русский

Для любого M и d с хотя бы двумя, M^H = OfNat(d) эквивалентно M = OfNat(d).

LaTeX

$$$M^{H} = \operatorname{OfNat}(d) \iff M = \operatorname{OfNat}(d)$$$

Lean4

@[simp]
theorem conjTranspose_eq_ofNat [DecidableEq n] [Semiring α] [StarRing α] {M : Matrix n n α} {d : ℕ} [d.AtLeastTwo] :
    Mᴴ = ofNat(d) ↔ M = OfNat.ofNat d :=
  conjTranspose_eq_natCast

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