Theorems · Theorem · functional analysis

LinearMap.normDet_eq_norm_det_toMatrix

∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] {ι : Type u_5} [inst_6 : Fintype ι] [inst_7 : DecidableEq ι] (f : U →ₗ[𝕜] V)
  (bu : OrthonormalBasis ι 𝕜 U) (bv : OrthonormalBasis ι 𝕜 V),
  f.normDet = ‖((LinearMap.toMatrix bu.toBasis bv.toBasis) f).det‖

LinearMap.normDet can be calculated with any pair of orthonormal basis if the domain and the codomain have equal dimension.

Defined in

Mathlib.Analysis.InnerProductSpace.NormDet

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensionalNormedAddCommGroupInnerProductSpaceFintypeDecidableEq