toMatrix_smul_left

Mathlib.LinearAlgebra.Matrix.Basis

URI: https://scilib.ai/kg/mathlib#Module.Basis.toMatrix_smul_left

← MathLib Explorer

English

If AB = 1 and all entries of B lie in a subfield K, then A's entries lie in K.

Русский

Если AB = 1 и все элементы B лежат в подполе K, то элементы A лежат в K.

LaTeX

$$If AB = 1 and (∀ i j, B_{i j} ∈ K), then (∀ i j, A_{i j} ∈ K).$$

Lean4

theorem toMatrix_smul_left {G} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) :
    (g • e).toMatrix v = e.toMatrix (g⁻¹ • v) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru