Skip to content

[Merged by Bors] - chore: tidy various files #19162

[Merged by Bors] - chore: tidy various files

[Merged by Bors] - chore: tidy various files #19162

Triggered via pull request August 11, 2023 18:59
Status Success
Total duration 44s
Artifacts

detect_sha_changes.yml

on: pull_request
Add annotations
33s
Add annotations
Fit to window
Zoom out
Zoom in

Annotations

1 notice
Synchronization: Mathlib/Analysis/NormedSpace/ContinuousLinearMap.lean#L8
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/analysis/normed_space/continuous_linear_map?range=41bef4ae1254365bc190aee63b947674d2977f01..fe18deda804e30c594e75a6e5fe0f7d14695289f