Commit 2023-12-05 18:54 bcd9607b

View on Github →

feat: Add API for AlgEquiv. (#8639)

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

added def AlgEquiv.algHomUnitsEquiv

added theorem AlgEquiv.one_toLinearMap

added theorem AlgEquiv.pow_toLinearMap

added theorem AlgEquiv.toAlgHom_toRingHom

added def AlgEquiv.toLinearMapHom

Modified Mathlib/Algebra/Algebra/Hom.lean

added theorem RingHom.toIntAlgHom_injective

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

added theorem MulEquivClass.toMulEquiv_injective

Modified Mathlib/Logic/Equiv/Defs.lean

added theorem EquivLike.coe_coe

Modified Mathlib/RepresentationTheory/Rep.lean