mathlib

3c72a10e - refactor(algebra/algebra/{pi,prod}): extract into new files (#17853)

refactor(algebra/algebra/{pi,prod}): extract into new files (#17853) This matches `group/pi` and `ring/pi` etc. The lemma `algebra.algebra_map_prod_apply` has been renamed to `prod.algebra_map_apply`. Everything else has been moved without changes.