Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-22 13:06 7d02c231

View on Github →

chore(linear_algebra/*): rename copair, pair to coprod, prod (#2213)

  • chore(linear_algebra/*): rename copair, pair to coprod, prod
  • add back mistakenly deleted lemma
  • fix sensitivity, change comments to module docs
  • docstrings, linting
  • Update archive/sensitivity.lean

Estimated changes

modified theorem linear_equiv.trans_apply
deleted def linear_map.copair
deleted theorem linear_map.copair_apply
deleted theorem linear_map.copair_inl
deleted theorem linear_map.copair_inl_inr
deleted theorem linear_map.copair_inr
added theorem linear_map.coprod_inl
added theorem linear_map.coprod_inr
deleted theorem linear_map.fst_eq_copair
deleted theorem linear_map.fst_pair
added theorem linear_map.fst_prod
deleted theorem linear_map.inl_eq_pair
added theorem linear_map.inl_eq_prod
deleted theorem linear_map.inr_eq_pair
added theorem linear_map.inr_eq_prod
deleted theorem linear_map.ker_pair
added theorem linear_map.ker_prod
deleted def linear_map.pair
deleted theorem linear_map.pair_apply
modified theorem linear_map.pair_fst_snd
modified def linear_map.prod
added theorem linear_map.prod_apply
deleted theorem linear_map.snd_eq_copair
deleted theorem linear_map.snd_pair
added theorem linear_map.snd_prod
modified theorem constr_smul
modified theorem is_basis_empty_bot