normalized_factors

Stream: maths

[Yury G. Kudryashov]

Why docs#unique_factorization_monoid.normalized_factors depends on decidable_eq? It is noncomputable anyway.

[Yury G. Kudryashov]

Same question about factors.

[Yury G. Kudryashov]

@Johannes Hölzl, @Jens Wagemaker, and @Aaron Anderson are listed as the authors of this file.

[Yury G. Kudryashov]

Also, I get "deterministic timeout" in docs#ideal.count_normalized_factors_eq (see also #14444 - one of the assumptions is not needed).

[Yury G. Kudryashov]

Ping here.

[Anne Baanen]

(Given our current definition of unique factorization monoid,) I'm happy if we delete the dec_eq even looking intuitionistically. Looks like there are no lemmas that would unfold the definition to expose a classical.dec_eq, so I think just an open_locale classical would work here with no complications.

[Anne Baanen]

Do I understand correctly that #14444 fixes the timeout?

[Yury G. Kudryashov]

No. I failed to understand why the timeout happens bot noticed that one assumption is not needed. Could you please adopt #14444?

[Anne Baanen]

Sure. I'm busy the coming weeks so hopefully I can find some time to investigate. If it's taking too long, I'm happy for someone else to take over before I get a chance, of course.

[Junyan Xu]

#14590 should fix the docs#unique_factorization_monoid.count_normalized_factors_eq timeout