mathlib3
14997d0e - feat(analysis/normed_space): allow non-unital C^* rings (#12327)

Commit

3 years ago

feat(analysis/normed_space): allow non-unital C^* rings (#12327) Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents