Eigenvalue coercion

Stream: mathlib4

[Jireh Loreaux]

As with other subtype synonyms in Lean 4, docs4#Module.End.Eigenvalues no longer automatically inherits the Subtype.val coercion from Eigenvalues f to R. This came up while porting analysis.inner_product_space.spectrum. Should I define Eigenvalues.val and set it up as a coercion?

[Eric Wieser]

Should it be reducible?

[Eric Wieser]

I don't see much point in declaring "an eigenvalues is a element that is an eigenvalue" an implementation detail

[Jireh Loreaux]

Probably, Lean also wasn't able to infer DecidableEq (Eigenvalues f) from DecidableEq R.

[Jireh Loreaux]

Oh, hah, I just found a porting note about the coercion. I think whoever ported that file didn't know about CoeOut, which is the appropriate class here.

[Jireh Loreaux]

I'm just going to add the necessary instances, but maybe we can make it reducible later if we run into more trouble.

[Eric Wieser]

We could try a backport, given it's only one line! I would guess it makes less work overall not more

[Eric Wieser]

Note we already made a similar change for module.dual when porting, so there's precedent for changing reducibility to help with porting

[Jireh Loreaux]

I've ported several files down the chain and the only extra thing I've needed thus far is the DecidableEq instance, and I'm almost to the leaf files. I'm okay with making it reducible, but let's either not bother with a backport, or not make reducible until after the port.