Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-20 19:46 a4108eb4

View on Github →

fix(algebra/pi_instances): bugfix

Estimated changes

Modified algebra/pi_instances.lean

Modified linear_algebra/prod_module.lean

deleted theorem is_basis_inl_union_inr

deleted theorem is_linear_map_prod_fst

deleted theorem is_linear_map_prod_inl

deleted theorem is_linear_map_prod_inr

deleted theorem is_linear_map_prod_mk

deleted theorem is_linear_map_prod_snd

deleted theorem linear_independent_inl_union_inr

added theorem prod.is_basis_inl_union_inr

added theorem prod.is_linear_map_prod_fst

added theorem prod.is_linear_map_prod_inl

added theorem prod.is_linear_map_prod_inr

added theorem prod.is_linear_map_prod_mk

added theorem prod.is_linear_map_prod_snd

added theorem prod.linear_independent_inl_union_inr

added theorem prod.span_inl_union_inr

added theorem prod.span_prod

deleted theorem span_inl_union_inr

deleted theorem span_prod