mathlib3
57cd1e9e - feat(analysis/normed_space/exponential): remove char_p assumption (#9618)

Commit
4 years ago
feat(analysis/normed_space/exponential): remove char_p assumption (#9618) Remove the `char_p` assumption from `exp_series_eq_exp_series_of_field_extension` as suggested by @urkud here : https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Undergraduate.20math.20list/near/256679511
Author
Parents
Loading