Theorem StarAlgHom.ext_adjoin_singleton

Modification history

2024-02-05 18:00

Mathlib/Algebra/Star/Subalgebra.lean

refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …

Modified StarAlgHom.ext_adjoin_singleton View on Github →

2023-03-12 21:48

Mathlib/Algebra/Star/Subalgebra.lean

feat: port Algebra.Star.Subalgebra (#2819) …

Added StarAlgHom.ext_adjoin_singleton View on Github →