Theorems · Theorem · commutative algebra

Matrix.det_det

∀ {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  (M : Matrix m m S) [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] [inst_4 : Fintype m] [inst_5 : Fintype n]
  (f : S →+* Matrix n n R), (f M.det).det = ((Matrix.comp m m n n R) (M.map ⇑f)).det

The main result in Silvester's paper Determinants of Block Matrices: the determinant of a block matrix with commuting, equal-sized, square blocks can be computed by taking determinants twice in a row: first take the determinant over the commutative ring generated by the blocks (S here), then take the determinant over the base ring.

Defined in

Mathlib.RingTheory.Norm.Transitivity

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingDecidableEqDecidableEqFintypeFintype