Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-24 09:18 4aacae31

View on Github →

feat(data/equiv/algebra): instances for transporting algebra across an equiv (#618)

Estimated changes

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