PR #19244 refactor: Remove the K argument from exp

refactor: Remove the K argument from exp #19244

eric-wieser wants to merge 8 commits into master from eric-wieser/exp-rat

feat(analysis/normed_space/exponential): Generalize `field` lemmas ab…

9c7f0987

authorship

48fc050b

fix blank line

fc42704c

fix

bcc9e98b

wip

a4558132

Merge remote-tracking branch 'origin/master' into eric-wieser/exp-rat

315c802b

Merge remote-tracking branch 'origin/master' into eric-wieser/exp-rat

b275b431

eric-wieser added too-late

eric-wieser changed the title ~~refactor: Remove the K argument from ext~~ refactor: Remove the K argument from exp 2 years ago

github-actions added modifies-synchronized-file

fix

b6a69bf4

eric-wieser closed this 2 years ago

YaelDillies deleted the eric-wieser/exp-rat branch 2 years ago

Reviewers

No reviews

Assignees

No one assigned

Labels

modifies-synchronized-file too-late

Milestone

No milestone