det_smul_of_tower — Mathlib

English

Let α be a monoid acting on a ring R with an IsScalarTower structure; for c ∈ α and A a square matrix over R, det(c • A) = c^{Fintype.card n} • det A.

Русский

Пусть α — моноид, действующий на кольцо R, с структурой IsScalarTower; при c ∈ α и A квадратная матрица над R выполняется det(c • A) = c^{Fintype.card n} • det A.

LaTeX

$$$$\det(c \cdot A) = c^{n} \cdot \det A, \quad n = Fintype.card\, n,$$ в общем виде через размер матрицы.$$

Lean4

@[simp]
theorem det_smul_of_tower {α} [Monoid α] [MulAction α R] [IsScalarTower α R R] [SMulCommClass α R R] (c : α)
    (A : Matrix n n R) : det (c • A) = c ^ Fintype.card n • det A := by
  rw [← smul_one_smul R c A, det_smul, smul_pow, one_pow, smul_mul_assoc, one_mul]

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