isAdjointPair_equiv' — Mathlib

English

Let B be a bilinear form on M, and b a basis. Then BilinForm.toMatrix b B transforms correctly under matrix operations via the underlying linear maps.

Русский

Пусть B — билинейная форма на M, и b — база. Тогда BilinForm.toMatrix b B корректно преобразуется под операциями над матрицами посредством соответствующих линейных отображений.

LaTeX

$$$$M \cdot \mathrm{BilinForm.toMatrix}_{b}(B) = \mathrm{BilinForm.toMatrix}_{b}\bigl(B \circ (\mathrm{Matrix.toLin}_{b b} M^{T})\bigr).$$$$

Lean4

theorem isAdjointPair_equiv' [DecidableEq n] (P : Matrix n n R₂) (h : IsUnit P) :
    (Pᵀ * J * P).IsAdjointPair (Pᵀ * J * P) A A' ↔ J.IsAdjointPair J (P * A * P⁻¹) (P * A' * P⁻¹) :=
  Matrix.isAdjointPair_equiv _ _ _ _ h

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