Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-26 07:39 7afdab63

View on Github →

refactor(data/equiv/algebra): rewrite ring_equiv using bundled homs (#1482)

  • refactor(data/equiv/algebra): rewrite ring_equiv using bundled homs Fix some compile errors
  • Fix compile, add missing docs
  • Docstrings
  • Use less ring_equiv.to_equiv outside of data/equiv/algebra
  • Join lines

Estimated changes

added theorem add_equiv.map_sub
added theorem mul_equiv.map_inv
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 def ring_equiv.of'
added def ring_equiv.of
deleted theorem ring_equiv.to_equiv_symm
modified structure ring_equiv
deleted theorem ring_equiv.map_add
deleted theorem ring_equiv.map_mul
deleted theorem ring_equiv.map_neg
deleted theorem ring_equiv.map_neg_one
deleted theorem ring_equiv.map_one
deleted theorem ring_equiv.map_sub
deleted theorem ring_equiv.map_zero