Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-29 22:06 4845b663

View on Github →

feat(ring_theory): free_ring and free_comm_ring (#734)

  • feat(ring_theory): free_ring and free_comm_ring
  • Define isomorphism with mv_polynomial int
  • Ring hom free_ring -> free_comm_ring; 1 sorry left
  • Coe from free_ring to free_comm_ring is ring_hom
  • WIP
  • WIP
  • WIP
  • WIP
  • Refactoring a bunch of stuff
  • functor.map_equiv
  • Fix build
  • Fix build
  • Make multiset.subsingleton_equiv computable
  • Define specific equivs using general machinery
  • Fix build
  • Remove old commented code
  • feat(data/equiv/functor): map_equiv
  • fix(data/multiset): remove duplicate setoid instance
  • namespace changes

Estimated changes

added theorem free_comm_ring.lift_of
added theorem free_comm_ring.map_add
added theorem free_comm_ring.map_mul
added theorem free_comm_ring.map_neg
added theorem free_comm_ring.map_of
added theorem free_comm_ring.map_one
added theorem free_comm_ring.map_pow
added theorem free_comm_ring.map_sub
added def free_comm_ring
added theorem free_ring.coe_eq
added def free_ring.lift
added theorem free_ring.lift_add
added theorem free_ring.lift_comp_of
added theorem free_ring.lift_mul
added theorem free_ring.lift_neg
added theorem free_ring.lift_of
added theorem free_ring.lift_one
added theorem free_ring.lift_pow
added theorem free_ring.lift_sub
added theorem free_ring.lift_zero
added def free_ring.map
added theorem free_ring.map_add
added theorem free_ring.map_mul
added theorem free_ring.map_neg
added theorem free_ring.map_of
added theorem free_ring.map_one
added theorem free_ring.map_pow
added theorem free_ring.map_sub
added theorem free_ring.map_zero
added def free_ring.of
added def free_ring