module module

`IndisputableMonolith.Cosmology.EntropyConservationFRW`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Cosmology.GrandPotential module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.NeutrinoDilution module_import

declarations in this module (10)

theorem continuity_from_friedmann L81
theorem comoving_entropy_conserved L128
theorem radiation_aT_conserved L168
theorem radiation_euler L196
theorem radiation_gibbs_duhem L201
theorem entropy_conserved_from_friedmann L214
theorem comoving_entropy_constant L234
theorem radiation_aT_constant L253
theorem dilution_from_frw L279
theorem gStarS_from_frw L316