This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
refactor: Remove the K argument from exp #7377
eric-wieseradd_ported_warnings.yml
on: pull_request
Check for modifications to ported files
26s
Annotations
1 warning
|
Check for modifications to ported files:
src/analysis/normed_space/exponential.lean#L1
Changes to this file will need to be ported to mathlib 4!
Please consider retracting the changes to this file unless you are willing to immediately forward-port them.
|