mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(analysis/normed_space/basic): the left-regular representation is an isometry for (even non-unital) C⋆-algebras

Open j-loreaux opened this issue 3 years ago • 1 comments

This is a key tool to show that the multiplier algebra is a C⋆-algebra.

  • [ ] depends on: #16963

Open in Gitpod

j-loreaux avatar Oct 13 '22 19:10 j-loreaux

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16963~~ By Dependent Issues (🤖). Happy coding!

mathlib-dependent-issues-bot avatar Oct 25 '22 03:10 mathlib-dependent-issues-bot

:v: j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors[bot] avatar Nov 08 '22 15:11 bors[bot]

bors merge

j-loreaux avatar Nov 09 '22 20:11 j-loreaux

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Nov 09 '22 23:11 bors[bot]