Theorem WithCStarModule.equiv_snd

Modification history

2025-03-30 16:02

Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean

refactor: default to left modules for `CStarModule` (#22967) …

Modified WithCStarModule.equiv_snd View on Github →

2024-08-15 08:47

Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean

feat: add the `WithCStarModule` type synonym (#15763) …

Added WithCStarModule.equiv_snd View on Github →