Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-04 11:56 494132e1

View on Github →

feat(algebra): commuting elements (#1089)

  • Not sure how this works
  • Small refactor of geometric sums
  • Properties of commuting elements
  • Geometric sums moved to geom_sum.lean
  • Geometric sums, two commuting variables
  • Import geom_sum.lean
  • Cover commuting elements of noncommutative rings
  • Whitespace
  • Add file headers
  • Delete stray file
  • Sum/prod over range 0, range 1
  • Add simp lemmas
  • Various changes from PR review
  • Add semigroup case
  • Changes from PR review
  • Corrected all_commute to commute.all
  • Minor changes from PR review
  • Change line endings back to unix
  • @[to_additive] can't be a local attribute
  • Rename add_pow_comm to add_pow_of_commute as suggested by @jcommelin
  • Add a few missing instances
  • DRY
  • Notation for gsmul should go into add_group, not group
  • Prove gsmul_one
  • Reorder algebra/commute, add more lemmas
  • Add docs, rename geom_sum₂_mul_add_comm to commute.geom_sum₂_mul_add.
  • Rename, add a docstring
  • Fix a typo spotted by @ChrisHughes24
  • Move common args to variables
  • Rename commute.mul to commute.mul_right etc.
  • Add some @[simp] attributes.
  • More @[simp]
  • Add some _iff versions

Estimated changes

added theorem finset.prod_range_one
added theorem finset.prod_range_zero
added theorem finset.sum_range_one
deleted theorem geom_sum
deleted theorem geom_sum_inv
deleted theorem geom_sum_mul
deleted theorem geom_sum_mul_add
added def centralizer
added theorem commute.add_left
added theorem commute.add_right
added theorem commute.cast_int_left
added theorem commute.cast_int_right
added theorem commute.cast_nat_left
added theorem commute.cast_nat_right
added theorem commute.gpow_gpow
added theorem commute.gpow_gpow_self
added theorem commute.gpow_left
added theorem commute.gpow_right
added theorem commute.gpow_self
added theorem commute.gsmul_gsmul
added theorem commute.gsmul_left
added theorem commute.gsmul_right
added theorem commute.gsmul_self
added theorem commute.inv_inv
added theorem commute.inv_inv_iff
added theorem commute.inv_left
added theorem commute.inv_left_iff
added theorem commute.inv_right
added theorem commute.inv_right_iff
added theorem commute.list_prod_left
added theorem commute.mul_left
added theorem commute.mul_right
added theorem commute.neg_left
added theorem commute.neg_left_iff
added theorem commute.neg_one_left
added theorem commute.neg_one_right
added theorem commute.neg_right
added theorem commute.neg_right_iff
added theorem commute.one_left
added theorem commute.one_right
added theorem commute.pow_left
added theorem commute.pow_pow
added theorem commute.pow_pow_self
added theorem commute.pow_right
added theorem commute.pow_self
added theorem commute.self_gpow
added theorem commute.self_gsmul
added theorem commute.self_pow
added theorem commute.self_smul
added theorem commute.self_smul_smul
added theorem commute.smul_left
added theorem commute.smul_right
added theorem commute.smul_self
added theorem commute.smul_smul
added theorem commute.sub_left
added theorem commute.sub_right
added theorem commute.units_coe
added theorem commute.units_inv_left
added theorem commute.zero_left
added theorem commute.zero_right
added def commute
added theorem mem_centralizer
added theorem neg_pow
added def geom_series
added theorem geom_series_def
added theorem geom_series_one
added theorem geom_series_zero
added def geom_series₂
added theorem geom_series₂_def
added theorem geom_series₂_one
added theorem geom_series₂_zero
added theorem geom_sum
added theorem geom_sum_inv
added theorem geom_sum_mul
added theorem geom_sum_mul_add
added theorem geom_sum_mul_neg
added theorem geom_sum₂_mul
added theorem geom_sum₂_mul_add
added theorem geom_sum₂_mul_comm
added theorem gsmul_one
modified theorem add_pow
added theorem commute.add_pow
deleted theorem is_submonoid.inter