Commit 2021-11-12 03:51 e5a79a7a

View on Github →

feat(analysis/normed_space/star): introduce C*-algebras (#10145) This PR introduces normed star rings/algebras and C*-rings/algebras, as well as a version of star bundled as a linear isometric equivalence.

Estimated changes

Modified src/algebra/star/module.lean

modified def star_linear_equiv

Created src/analysis/normed_space/star.lean

added theorem coe_starₗᵢ

added theorem cstar_ring.norm_self_mul_star

added theorem cstar_ring.norm_star_mul_self'

added def starₗᵢ

added theorem starₗᵢ_apply