IndisputableMonolith.Relativity.ILG.LensingDerived
IndisputableMonolith/Relativity/ILG/LensingDerived.lean · 25 lines · 0 declarations
show as:
view math explainer →
1/-!
2Temporarily deferred: ILG Lensing-derived module
3
4This module is intentionally disabled to reduce scope for the current
5milestone. All previous imports and declarations are commented out.
6Re-enable by restoring the original contents when ready.
7-/
8
9-- import Mathlib
10-- import IndisputableMonolith.Relativity.ILG.Action
11-- import IndisputableMonolith.Relativity.Lensing.Deflection
12-- import IndisputableMonolith.Relativity.Lensing.TimeDelay
13-- import IndisputableMonolith.Relativity.Lensing.ClusterPredictions
14-- import IndisputableMonolith.Relativity.PostNewtonian.GammaExtraction
15
16-- namespace IndisputableMonolith
17-- namespace Relativity
18-- namespace ILG
19
20-- (Intentionally left empty while deferred)
21
22-- end ILG
23-- end Relativity
24-- end IndisputableMonolith
25