mem_skewAdjointMatricesLieSubalgebra_unit_smul

English

For a unit u in the base ring, membership in the skewAdjointMatricesLieSubalgebra is invariant under scaling of J by u.

Русский

При масштабировании матрицы J единицей u принадлежность в кососопряжённых сохраняется.

LaTeX

$$$A \in skewAdjointMatricesLieSubalgebra (u \cdot J) \iff A \in skewAdjointMatricesLieSubalgebra J$$$

Lean4

theorem mem_skewAdjointMatricesLieSubalgebra_unit_smul (u : Rˣ) (J A : Matrix n n R) :
    A ∈ skewAdjointMatricesLieSubalgebra (u • J) ↔ A ∈ skewAdjointMatricesLieSubalgebra J :=
  by
  change A ∈ skewAdjointMatricesSubmodule (u • J) ↔ A ∈ skewAdjointMatricesSubmodule J
  simp only [mem_skewAdjointMatricesSubmodule, Matrix.IsSkewAdjoint, Matrix.IsAdjointPair]
  constructor <;> intro h
  · simpa using congr_arg (fun B => u⁻¹ • B) h
  · simp [h]

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