`IndisputableMonolith.Astrophysics.CosmicMagneticFieldsStructure`

IndisputableMonolith/Astrophysics/CosmicMagneticFieldsStructure.lean · 22 lines · 3 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Astrophysics.FRBStructure
   3
   4namespace IndisputableMonolith
   5namespace Astrophysics
   6namespace CosmicMagneticFieldsStructure
   7
   8open FRBStructure
   9
  10def cosmic_magnetic_fields_from_ledger : Prop := frb_from_ledger
  11
  12theorem cosmic_magnetic_fields_structure : cosmic_magnetic_fields_from_ledger := frb_structure
  13
  14/-- Cosmic-magnetic-field structure implies FRB-side structural input. -/
  15theorem cosmic_magnetic_fields_implies_frb (h : cosmic_magnetic_fields_from_ledger) :
  16    frb_from_ledger :=
  17  h
  18
  19end CosmicMagneticFieldsStructure
  20end Astrophysics
  21end IndisputableMonolith
  22

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