Skip to content
Detect changes to header SHAs

[Merged by Bors] - feat: Self-adjoint LinearPMaps are densely defined #16873

Sign in to view logs

[Merged by Bors] - feat: Self-adjoint LinearPMaps are densely defined

[Merged by Bors] - feat: Self-adjoint LinearPMaps are densely defined #16873

Triggered via pull request July 25, 2023 14:36
@mcdollmcdoll
synchronize #6075
mcdoll/self_adjoint
Status Success
Total duration 46s
Artifacts –

detect_sha_changes.yml

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

Annotations

3 notices
Synchronization: Mathlib/RingTheory/Ideal/Cotangent.lean#L12
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/ideal/cotangent?range=70fd9563a21e7b963887c9360bd29b2393e6225a..4b92a463033b5587bb011657e25e4710bfca7364
Synchronization: Mathlib/RingTheory/Kaehler.lean#L10
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/ring_theory/kaehler?range=b608348ffaeb7f557f2fd46876037abafd326ff3..4b92a463033b5587bb011657e25e4710bfca7364
Synchronization: Mathlib/Topology/MetricSpace/Basic.lean#L11
See review instructions and diff at https://leanprover-community.github.io/mathlib-port-status/file/topology/metric_space/basic?range=8000bbbe2e9d39b84edb993d88781f536a8a3fa8..8047de4d911cdef39c2d646165eea972f7f9f539