basic): make prop type classes props (#12233)

Commit

4 years ago

fix(analysis/normed_space/star/basic): make prop type classes props (#12233) The type classes `normed_star_monoid` and `cstar_ring` are now properly declared as prop.

Author

dupuisf

Parents

264dd7ff

mathlib e77675d2 - fix(analysis/normed_space/star/basic): make prop type classes props (#12233)

mathlib
e77675d2 - fix(analysis/normed_space/star/basic): make prop type classes props (#12233)