mathlib3
9fb9fb15 - chore(analysis/normed_space): golf `normed_algebra.nontrivial`

Commit

3 years ago

chore(analysis/normed_space): golf `normed_algebra.nontrivial`

References

eric-wieser/norm_one_class.nontrivial

Author

eric-wieser

eric-wieser

Parents

Loading