Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-09-15 17:29 39bab47f

View on Github →

feat(linear_algebra): dimension theorem (#345)

  • dimension theorem
  • more theorems about dimension
  • cardinal stuff
  • fix error
  • move A/S x S = A to quotient_module.lean
  • remove pempty_equiv_empty

Estimated changes

added def equiv.prod_punit
added theorem equiv.prod_punit_apply
deleted def equiv.prod_unit
deleted theorem equiv.prod_unit_apply
added def equiv.punit_prod
added theorem equiv.punit_prod_apply
deleted def equiv.unit_prod
deleted theorem equiv.unit_prod_apply
added theorem fintype.card_punit
added theorem fintype.univ_punit
added theorem is_basis.linear_equiv
added theorem vector_space.dim_prod
added theorem vector_space.mk_basis
added theorem cardinal.finset_card
added theorem cardinal.mk_Prop
added theorem cardinal.mk_bool
added theorem cardinal.mk_empty'
added theorem cardinal.mk_empty
added theorem cardinal.mk_option
added theorem cardinal.mk_pempty
added theorem cardinal.mk_plift_true
added theorem cardinal.mk_punit
added theorem cardinal.mk_singleton
added theorem cardinal.mk_unit
added theorem cardinal.mk_list_eq_mk
added theorem cardinal.pow_le