Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-22 07:48 aba31c93

View on Github →

feat(algebra/monoid_algebra): define a non-commutative version of lift (#4725)

  • define monoid_algebra.lift_c and add_monoid_algebra.lift_nc to be generalizations of (mv_)polynomial.eval₂ to (add_)monoid_algebras.
  • use to_additive in many proofs about add_monoid_algebra;
  • define finsupp.nontrivial, use it for (add_)monoid_algebra.nontrivial;
  • copy more lemmas about lift from monoid_algebra to add_monoid_algebra;
  • use @[ext] on more powerful type-specific lemmas;
  • fix docstrings of (add_)monoid_algebra.lift₂;
  • fix compile failures.

Estimated changes

modified theorem add_monoid_algebra.of_apply
modified theorem monoid_algebra.alg_hom_ext
added theorem finsupp.sum_add_index'
modified theorem mv_polynomial.alg_hom_ext
deleted theorem mv_polynomial.eval_unique
modified theorem mv_polynomial.ring_hom_ext