Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-08 18:41 3c72a10e

View on Github →

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.

Estimated changes

deleted theorem alg_hom.coe_prod
deleted def alg_hom.fst
deleted theorem alg_hom.fst_prod
deleted def alg_hom.prod
deleted def alg_hom.prod_equiv
deleted theorem alg_hom.prod_fst_snd
deleted def alg_hom.snd
deleted theorem alg_hom.snd_prod
deleted theorem pi.algebra_map_apply
deleted theorem pi.algebra_map_def
deleted def pi.const_alg_hom
deleted def pi.eval_alg_hom
added theorem pi.algebra_map_apply
added theorem pi.algebra_map_def
added def pi.const_alg_hom
added def pi.eval_alg_hom
added theorem alg_hom.coe_prod
added def alg_hom.fst
added theorem alg_hom.fst_prod
added def alg_hom.prod
added theorem alg_hom.prod_fst_snd
added def alg_hom.snd
added theorem alg_hom.snd_prod
added theorem prod.algebra_map_apply