Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-06 03:49 15c434a2

View on Github →

chore(*): various simple lemmas about *_equiv, add missing attrs (#1854)

  • chore(*): various simple lemmas about *_equiv, add missing attrs
  • Fix compile of ring_theory/localization

Estimated changes

modified theorem mul_equiv.map_eq_one_iff
modified theorem mul_equiv.map_ne_one_iff
modified theorem ring_equiv.map_add
modified theorem ring_equiv.map_mul
modified theorem ring_equiv.map_neg
modified theorem ring_equiv.map_neg_one
modified theorem ring_equiv.map_one
modified theorem ring_equiv.map_sub
modified theorem ring_equiv.map_zero
added theorem set.inj_on.to_bij_on
added theorem linear_equiv.map_add
added theorem linear_equiv.map_neg
added theorem linear_equiv.map_smul
added theorem linear_equiv.map_sub
added theorem linear_equiv.map_zero
modified def linear_equiv.refl
modified def linear_equiv.symm
modified def linear_equiv.trans