Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-20 19:21 9aec1d18

View on Github →

refactor(algebra/pi_instances): move prod instances to pi_instances file

Estimated changes

added theorem prod.fst_inl
added theorem prod.fst_inr
added theorem prod.fst_inv
added theorem prod.fst_mul
added theorem prod.fst_one
added theorem prod.fst_prod
added theorem prod.injective_inl
added theorem prod.injective_inr
added def prod.inl
added theorem prod.inl_eq_inl
added theorem prod.inl_eq_inr
added def prod.inr
added theorem prod.inr_eq_inl
added theorem prod.inr_eq_inr
added theorem prod.snd_inl
added theorem prod.snd_inr
added theorem prod.snd_inv
added theorem prod.snd_mul
added theorem prod.snd_one
added theorem prod.snd_prod
added theorem is_basis_inl_union_inr
added theorem is_linear_map_prod_fst
added theorem is_linear_map_prod_inl
added theorem is_linear_map_prod_inr
added theorem is_linear_map_prod_mk
added theorem is_linear_map_prod_snd
deleted theorem prod.fst_inl
deleted theorem prod.fst_inr
deleted theorem prod.fst_inv
deleted theorem prod.fst_mul
deleted theorem prod.fst_one
deleted theorem prod.fst_prod
deleted theorem prod.injective_inl
deleted theorem prod.injective_inr
deleted def prod.inl
deleted theorem prod.inl_eq_inl
deleted theorem prod.inl_eq_inr
deleted def prod.inr
deleted theorem prod.inr_eq_inl
deleted theorem prod.inr_eq_inr
deleted theorem prod.snd_inl
deleted theorem prod.snd_inr
deleted theorem prod.snd_inv
deleted theorem prod.snd_mul
deleted theorem prod.snd_one
deleted theorem prod.snd_prod
deleted theorem prod.span_inl_union_inr
deleted theorem prod.span_prod
added theorem span_inl_union_inr
added theorem span_prod