mathlib documentation

algebra.hom.equiv.type_tags

Additive and multiplicative equivalences associated to multiplicative and additive. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.