Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-20 15:42 14024a3e

View on Github →

feat(linear_algebra/bilinear_form, linear_algebra/sesquilinear_form, ring_theory/maps): bilinear/sesquilinear forms (#1300)

  • Create involution.lean
  • Update involution.lean
  • Update involution.lean
  • Rename involution.lean to maps.lean
  • Create bilinear_form.lean
  • Create sesquilinear_form.lean
  • Update sesquilinear_form.lean
  • Style fixes
  • Update sesquilinear_form.lean
  • Style fixes
  • fix typo

Estimated changes

added theorem alt_bilin_form.neg
added theorem bilin_form.add_left
added theorem bilin_form.add_right
added theorem bilin_form.ext
added theorem bilin_form.neg_left
added theorem bilin_form.neg_right
added theorem bilin_form.ortho_zero
added theorem bilin_form.smul_left
added theorem bilin_form.smul_right
added theorem bilin_form.sub_left
added theorem bilin_form.sub_right
added theorem bilin_form.zero_left
added theorem bilin_form.zero_right
added structure bilin_form
added theorem sym_bilin_form.is_refl
added theorem sym_bilin_form.sym
added theorem alt_sesq_form.neg
added theorem refl_sesq_form.eq_zero
added theorem sesq_form.add_left
added theorem sesq_form.add_right
added theorem sesq_form.ext
added theorem sesq_form.neg_left
added theorem sesq_form.neg_right
added theorem sesq_form.ortho_zero
added theorem sesq_form.smul_left
added theorem sesq_form.smul_right
added theorem sesq_form.sub_left
added theorem sesq_form.sub_right
added theorem sesq_form.zero_left
added theorem sesq_form.zero_right
added structure sesq_form
added theorem sym_sesq_form.is_refl
added theorem sym_sesq_form.sym
added structure ring_anti_equiv
added theorem ring_equiv.bijective
added theorem ring_equiv.map_add
added theorem ring_equiv.map_mul
added theorem ring_equiv.map_neg
added theorem ring_equiv.map_neg_one
added theorem ring_equiv.map_one
added theorem ring_equiv.map_sub
added theorem ring_equiv.map_zero
added theorem ring_invo.bijective
added theorem ring_invo.map_add
added theorem ring_invo.map_mul
added theorem ring_invo.map_neg
added theorem ring_invo.map_neg_one
added theorem ring_invo.map_one
added theorem ring_invo.map_sub
added theorem ring_invo.map_zero
added theorem ring_invo.map_zero_iff
added structure ring_invo