Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-14 17:09 7b2be40f

View on Github →

refactor(data/equiv/algebra): split (#2147)

  • refactor(data/equiv/algebra): split I want to use ≃* without importing ring.
  • Update src/data/equiv/ring.lean

Estimated changes

deleted def add_aut.to_perm
deleted theorem add_equiv.map_sub
deleted structure add_equiv
deleted theorem equiv.add_def
deleted theorem equiv.inv_def
deleted theorem equiv.mul_def
deleted theorem equiv.neg_def
deleted theorem equiv.one_def
deleted theorem equiv.zero_def
deleted def mul_aut.to_perm
deleted def mul_aut
deleted theorem mul_equiv.ext
deleted theorem mul_equiv.map_eq_one_iff
deleted theorem mul_equiv.map_inv
deleted theorem mul_equiv.map_mul
deleted theorem mul_equiv.map_ne_one_iff
deleted theorem mul_equiv.map_one
deleted def mul_equiv.mk'
deleted def mul_equiv.refl
deleted def mul_equiv.symm
deleted theorem mul_equiv.to_equiv_symm
deleted def mul_equiv.trans
deleted structure mul_equiv
deleted def ring_aut.to_add_aut
deleted def ring_aut.to_mul_aut
deleted def ring_aut.to_perm
deleted def ring_aut
deleted theorem ring_equiv.coe_add_equiv
deleted theorem ring_equiv.coe_mul_equiv
deleted theorem ring_equiv.ext
deleted theorem ring_equiv.map_add
deleted theorem ring_equiv.map_eq_one_iff
deleted theorem ring_equiv.map_mul
deleted theorem ring_equiv.map_ne_one_iff
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
deleted def ring_equiv.of'
deleted def ring_equiv.of
deleted structure ring_equiv
deleted def to_units
deleted def units.map_equiv
added def add_aut.to_perm
added theorem add_equiv.map_sub
added structure add_equiv
added def mul_aut.to_perm
added def mul_aut
added theorem mul_equiv.ext
added theorem mul_equiv.map_inv
added theorem mul_equiv.map_mul
added theorem mul_equiv.map_one
added def mul_equiv.mk'
added def mul_equiv.refl
added def mul_equiv.symm
added def mul_equiv.trans
added structure mul_equiv
added def to_units
added def units.map_equiv
added def ring_aut.to_perm
added def ring_aut
added theorem ring_equiv.ext
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
added structure ring_equiv
added theorem equiv.add_def
added theorem equiv.inv_def
added theorem equiv.mul_def
added theorem equiv.neg_def
added theorem equiv.one_def
added theorem equiv.zero_def