Commit 2023-04-19 09:11 34a32cd4

View on Github →

feat: port Logic.Equiv.TransferInstance (#3206)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Equiv/TransferInstance.lean

added def Equiv.algEquiv

added theorem Equiv.div_def

added theorem Equiv.inv_def

added def Equiv.linearEquiv

added def Equiv.mulEquiv

added theorem Equiv.mulEquiv_apply

added theorem Equiv.mulEquiv_symm_apply

added theorem Equiv.mul_def

added theorem Equiv.one_def

added theorem Equiv.pow_def

added def Equiv.ringEquiv

added theorem Equiv.ringEquiv_apply

added theorem Equiv.ringEquiv_symm_apply

added theorem Equiv.smul_def