Irreducibility under algebra isomorphisms

Irreducibility of a polynomial after extending its coefficients is invariant under an isomorphism of algebras over the coefficient ring.

theorem TauCeti.irreducible_map_iff_of_algEquiv {F : Type u_1} {K : Type u_2} {K' : Type u_3} [CommSemiring F] [Semiring K] [Semiring K'] [Algebra F K] [Algebra F K'] (ψ : K ≃ₐ[F] K') (g : Polynomial F) : Irreducible (Polynomial.map (algebraMap F K) g) ↔ Irreducible (Polynomial.map (algebraMap F K') g)

Extending coefficients to isomorphic algebras preserves irreducibility.