Theorems · Theorem · linear algebra

LinearMap.det_eq_det_toMatrix_of_finset

∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M]
  [inst_3 : DecidableEq M] {s : Finset M} (b : Module.Basis (↥s) A M) (f : M →ₗ[A] M),
  LinearMap.det f = ((LinearMap.toMatrix b b) f).det

Defined in

Mathlib.LinearAlgebra.Determinant

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommGroupCommRingModuleDecidableEq