Theorems · Theorem · functional analysis

LinearMap.normDet_eq_norm_det_toMatrix_rangeRestrict

∀ {𝕜 : 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 ι 𝕜 ↥f.range),
  f.normDet = ‖((LinearMap.toMatrix bu.toBasis bv.toBasis) f.rangeRestrict).det‖

LinearMap.normDet is well-defined under any pair of orthonormal basis.

Defined in

Mathlib.Analysis.InnerProductSpace.NormDet

Cited by

8 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensionalNormedAddCommGroupInnerProductSpaceFintypeDecidableEq