running linter locally

Stream: general

[Gihan Marasingha]

The CI linter noticed unused instance arguments in my latest PR, but typing #lint in the file locally didn't show up the problems. These were duplicates of instances introduced by a previous variable declaration.

Am I using the linter incorrectly?

Edit: follow-up question: can one run the linter on a file or project as a stand-alone command from the terminal?

Anyway, once this (and any other issues that arise in the review process) is fixed, we should have Bessel's inequality. Thanks to @Heather Macbeth for suggesting the problem and for helpful advice.

The only thing I'm suspicious of is that I didn't need to use completeness of the inner product space.

Edit: for the past 1hr19 minutes, it has been my birthday.

[Heather Macbeth]

Gihan Marasingha said:

The only thing I'm suspicious of is that I didn't need to use completeness of the inner product space.

I don't know the answer to the question about the linter, but regarding the mathematical question -- I guess it's enough that the scalar field 𝕜 (which is ℝ or ℂ) is complete!