Theorems · Theorem · linear algebra

Matrix.isAdjointPair_equiv

∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J A₁ A₂ : Matrix n n R)
  [inst_2 : DecidableEq n] (P : Matrix n n R),
  IsUnit P →
    ((P.transpose * J * P).IsAdjointPair (P.transpose * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹))

Defined in

Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Cited by

1 results in Mathlib

Foundations

Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFintypeDecidableEq