mathlib3
16be8e39 - refactor(analysis/normed_space): simpler proof of `norm_sub_pow_two` (#6035)

Commit

4 years ago

refactor(analysis/normed_space): simpler proof of `norm_sub_pow_two` (#6035) Co-authors: `lean-gptf`, Stanislas Polu

Author

Jesse Michael Han

Parents