Commit 2024-08-23 01:24 e6c72d0a

View on Github →

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

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

deleted def WithCStarModule.equivOfInnerₗᵢ

deleted def WithCStarModule.equivₗᵢ

modified theorem WithCStarModule.inner_def

deleted theorem WithCStarModule.inner_eq_inner

deleted theorem WithCStarModule.norm_equiv

deleted theorem WithCStarModule.norm_equiv_of_inner

Modified Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean