Commit 2025-08-28 20:04 9c91a387

View on Github →

refactor: change unitary.map to take an explicit morphism as an argument, rather than a morphism class (#28122) This also defines unitary.mapEquiv as the induced equivalence on unitary groups, and provides various functoriality lemmas for both definitions.

Estimated changes

Modified Mathlib/Algebra/Star/MonoidHom.lean

added theorem StarMulEquiv.toMulEquiv_symm

added theorem StarMulEquiv.toMulEquiv_trans

added def StarMulEquiv.toStarMonoidHom

Modified Mathlib/Algebra/Star/Unitary.lean

added theorem unitary.coe_map

added theorem unitary.coe_map_star

modified def unitary.map

added def unitary.mapEquiv

added theorem unitary.mapEquiv_refl

added theorem unitary.mapEquiv_symm

added theorem unitary.mapEquiv_trans

added theorem unitary.map_comp

added theorem unitary.map_id

added theorem unitary.map_injective

modified theorem unitary.map_mem

added theorem unitary.toMonoidHom_mapEquiv

modified theorem unitary.toUnits_comp_map