Commit 2025-01-29 10:27 9219f8aa
View on Github →feat(RingTheory/IntegralClosure): product of integral algebras is integral (#21191) Pair of integral elements is an integral element of the product algebra. Product of integral algebras is an integral algebra.