mathlib3
2b2edc97 - chore(analysis/normed_space/basic): use explicit arg `𝕜'` in lemmas about `normed_algebra` (#6009)

Commit
4 years ago
chore(analysis/normed_space/basic): use explicit arg `𝕜'` in lemmas about `normed_algebra` (#6009)
Author
Parents
Loading