Commit 2022-12-12 09:20 506c7567

View on Github →

feat: port Algebra.Hom.Equiv.TypeTags (#943) mathlib3 SHA: 3342d1b2178381196f818146ff79bc0e7ccd9e2d

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Hom/Equiv/Basic.lean

Created Mathlib/Algebra/Hom/Equiv/TypeTags.lean

added def AddEquiv.additiveMultiplicative

added def AddEquiv.toMultiplicative''

added def AddEquiv.toMultiplicative'

added def AddEquiv.toMultiplicative

added def MulEquiv.multiplicativeAdditive

added def MulEquiv.toAdditive''

added def MulEquiv.toAdditive'

added def MulEquiv.toAdditive