autogenerated instance names

Stream: general

[Johan Commelin]

Some names seem suboptimal: docs#algebra.tensor_product.tensor_product.algebra

[Eric Wieser]

To be fair the instance is declared in the algebra.tensor_product namespace to begin with

[Eric Wieser]

So the outlook of an acceptable name is already somewhat bleak to begin with.

[Johan Commelin]

Hmm, I thought that the autogenerated names were placed in the root namespace... I guess I'm wrong (-;

[Eric Wieser]

I think it matches the autogenerated name against the current namespace and eliminates a common prefix, which prevents things like nat.nat.ring

[Yaël Dillies]

Another funny one: docs#ideal.mv_polynomial.mv_polynomial.ideal.is_jacobson

[FR]

Yet another: docs#polynomial.is_splitting_field.polynomial.splitting_field.finite_dimensional