Theorem WithCStarModule.inner_eq_inner

Modification history

2024-08-23 01:24

Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

refactor: remove `C⋆ᵐᵒᵈ` for C⋆-algebras and inner product spaces (#16048)

Deleted WithCStarModule.inner_eq_inner View on Github →

2024-08-19 19:19

Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

feat: constructions of Hilbert C⋆-modules (#15765) …

Added WithCStarModule.inner_eq_inner View on Github →