Post #2735441

@oantolin@mathstodon.xyz @boarders@mathstodon.xyz if you interpret FTAlgebra as "a polynomial over ℂ always has a factorisation into linear factors", then there's a natural uniqueness clause you could imagine adding on the end – and in fact it looks suspiciously like the one in FTArithmetic! Of course the result that a polynomial can't have two different factorisations into linear factors has nothing to do with ℂ in particular – it's true over any field, or even integral domain. But then, that would have made sense in the original context – it would explain why @byorgey@mathstodon.xyz had only done the other part so far, because they're not very related, so doing one doesn't help you much with the other. :-)