Theorems · Theorem · linear algebra

Matrix.submonoidCenter_eq_scalar_map

∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α],
  Submonoid.center (Matrix n n α) = Submonoid.map (Matrix.scalar n) (Submonoid.center α)

Defined in

Mathlib.Data.Matrix.Basis

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeSemiring