mem_selfAdjointMatricesSubmodule — Mathlib

English

Equivalence of adjointness under a basis change via an invertible P: (Pᵀ J P) IsAdjointPair (Pᵀ J P) A₁ A₂ ↔ J.IsAdjointPair J (P A₁ P⁻¹) (P A₂ P⁻¹).

Русский

Эквивалентность сопряженности при замене базиса через неособ. P: (Pᵀ J P) IsAdjointPair (Pᵀ J P) A₁ A₂ ↔ J.IsAdjointPair J (P A₁ P⁻¹) (P A₂ P⁻¹).

LaTeX

$$$ (P^T J P) IsAdjointPair (P^T J P) A_1 A_2 \\iff J IsAdjointPair J (P A_1 P^{-1}) (P A_2 P^{-1}).$$$

Lean4

@[simp]
theorem mem_selfAdjointMatricesSubmodule : A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁ := by
  rw [selfAdjointMatricesSubmodule, mem_pairSelfAdjointMatricesSubmodule, Matrix.IsSelfAdjoint]

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