pith. machine review for the scientific record. sign in

IndisputableMonolith.Relativity.ILG.LensingDerived

IndisputableMonolith/Relativity/ILG/LensingDerived.lean · 25 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   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

source mirrored from github.com/jonwashburn/shape-of-logic