mathlib
64b794a0 - chore(analysis/complex/basic): rename `complex/normed_space` (#9366)

Commit
4 years ago
chore(analysis/complex/basic): rename `complex/normed_space` (#9366) This matches `module.complex_to_real`
Author
Parents
Loading