Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Add mathlib4 porting warnings

refactor: Remove the K argument from exp #7378

Sign in to view logs

refactor: Remove the K argument from exp

refactor: Remove the K argument from exp #7378

Triggered via pull request November 12, 2023 12:55
@eric-wiesereric-wieser
synchronize #19244
eric-wieser/exp-rat
Status Success
Total duration 32s
Artifacts –

add_ported_warnings.yml

on: pull_request
Check for modifications to ported files
22s
Check for modifications to ported files
Fit to window
Zoom out
Zoom in

Annotations

2 warnings
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.
Check for modifications to ported files: src/analysis/normed_space/matrix_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.