Zulip Chat Archive
Stream: general
Topic: orthonormal_basis_index
Yaël Dillies (Sep 29 2022 at 07:48):
Why is docs#orthonormal_basis_index a thing? It can safely be replaced by fin (finrank 𝕜 E), right?
Yaël Dillies (Sep 29 2022 at 07:49):
In fact, that would let us unify docs#std_orthonormal_basis and docs#fin_std_orthonormal_basis.
Johan Commelin (Sep 29 2022 at 07:51):
Modulo DTT issues about fin n and fin (finrank K E) not being defeq for n = finrank K E.
Yaël Dillies (Sep 29 2022 at 07:54):
Not quite sure what purpose that serves, because you should never need defeq on an indexing type. What you could need is its size but having it fin (finrank 𝕜 E) gives it anyway.
Johan Commelin (Sep 29 2022 at 07:55):
One examply where it might matter is in induction arguments.
Johan Commelin (Sep 29 2022 at 07:56):
But I think that in 99% of the cases, I agree with your claim that the precise defeqs of an indexing type shouldn't matter.
Yaël Dillies (Sep 29 2022 at 07:58):
Currently fin_orthonormal_std_basis is only used twice (in the same file as it's defined in) and in both cases it could be replaced by a rw + orthonormal_std_basis. I'm happy to leave it as is but it is quite weird to have such a specific construction when nothing uses it.
Johan Commelin (Sep 29 2022 at 07:58):
No, I think you can certainly unify the two.
Yaël Dillies (Sep 29 2022 at 07:59):
Watch out for the #queue then :wink:
Johan Commelin (Sep 29 2022 at 07:59):
If someone needs a more generic fin n, then generalize or some fin.congr can probably make that work without too much effort.
Yaël Dillies (Sep 29 2022 at 08:30):
Last updated: Dec 20 2023 at 11:08 UTC