FormalConjecturesForMathlib/Analysis/Matrix/Spectrum.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 2 files
  1. def Matrix.IsHermitian.maxEigenvalue line 22 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: RCLike, Fintype, DecidableEq, Matrix, Matrix.IsHermitian, Real

    Proof uses: iSup, Matrix.IsHermitian.eigenvalues

    29 instances, coercions and auxiliary constants left out.