Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-23 18:29 2d395a99

View on Github →

refactor(algebra/pi_instance): delete pi_instance file, and move instances to group/ring etc appropriately (#3513)

Estimated changes

added theorem finset.prod_apply
added theorem finset.univ_sum_single
added theorem pi.list_prod_apply
added theorem pi.multiset_prod_apply
added theorem prod.fst_prod
added theorem prod.snd_prod
added theorem prod_mk_prod
added theorem ring_hom.functions_ext
added def monoid_hom.apply
added theorem monoid_hom.apply_apply
added theorem pi.inv_apply
added theorem pi.mul_apply
added theorem pi.one_apply
added def pi.single
added theorem pi.single_eq_of_ne
added theorem pi.single_eq_same
added theorem pi.sub_apply
added theorem pi.smul_apply'
added theorem pi.smul_apply
added theorem prod.smul_fst
added theorem prod.smul_mk
added theorem prod.smul_snd
deleted theorem finset.prod_apply
deleted theorem finset.prod_mk_prod
deleted theorem finset.univ_sum_single
deleted def monoid_hom.apply
deleted theorem monoid_hom.apply_apply
deleted theorem pi.finset_prod_apply
deleted theorem pi.inv_apply
deleted theorem pi.list_prod_apply
deleted theorem pi.mul_apply
deleted theorem pi.multiset_prod_apply
deleted theorem pi.one_apply
deleted def pi.single
deleted theorem pi.single_eq_of_ne
deleted theorem pi.single_eq_same
deleted theorem pi.smul_apply'
deleted theorem pi.smul_apply
deleted theorem pi.sub_apply
deleted theorem prod.fst.is_group_hom
deleted theorem prod.fst.is_monoid_hom
deleted theorem prod.fst_inl
deleted theorem prod.fst_inr
deleted theorem prod.fst_prod
deleted def prod.inl
deleted theorem prod.inl_eq_inl
deleted theorem prod.inl_eq_inr
deleted theorem prod.inl_injective
deleted def prod.inr
deleted theorem prod.inr_eq_inl
deleted theorem prod.inr_eq_inr
deleted theorem prod.inr_injective
deleted theorem prod.smul_fst
deleted theorem prod.smul_mk
deleted theorem prod.smul_snd
deleted theorem prod.snd.is_group_hom
deleted theorem prod.snd.is_monoid_hom
deleted theorem prod.snd_inl
deleted theorem prod.snd_inr
deleted theorem prod.snd_prod
deleted def ring_hom.apply
deleted theorem ring_hom.apply_apply
deleted theorem ring_hom.functions_ext
added def ring_hom.apply
added theorem ring_hom.apply_apply
modified def linear_map.inl
modified def linear_map.inr