Theorem StarAlgEquiv.toAlgEquiv_injective

Modification history

2025-12-22 13:19

Mathlib/Algebra/Star/StarAlgHom.lean

chore(Algebra): fix whitespace (#33182) …

Modified StarAlgEquiv.toAlgEquiv_injective View on Github →

2025-09-04 11:48

Mathlib/Algebra/Star/StarAlgHom.lean

feat(Algebra/Star/StarAlgHom): some API for `StarAlgEquiv` (#28881) …

Added StarAlgEquiv.toAlgEquiv_injective View on Github →