exponential): Weaken typeclass requirements (#13444)

Commit

3 years ago

feat(analysis/normed_space/exponential): Weaken typeclass requirements (#13444) This allows the exponential to be defined independently of a choice of norm.

Author

eric-wieser

Parents

2b902eb3

mathlib3 06a6044f - feat(analysis/normed_space/exponential): Weaken typeclass requirements (#13444)

mathlib3
06a6044f - feat(analysis/normed_space/exponential): Weaken typeclass requirements (#13444)