module module

`IndisputableMonolith.Cosmology.GrandPotential`

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.PhaseSpaceReduction module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cosmology.EntropyConservationFRW module_import
IndisputableMonolith.Cosmology.FermionWeightIntegral module_import
IndisputableMonolith.Cosmology.RadiationEntropyRelation module_import

declarations in this module (17)

def energyOf L88
theorem potential_euler L92
theorem potential_gibbs_duhem L100
theorem potential_entropy_deriv L108
theorem energy_deriv L118
theorem potential_energy_deriv L132
theorem potential_entropy_conserved L147
theorem potential_entropy_constant L168
def plasmaPressure L189
def plasmaEnergy L197
theorem plasmaPressure_eq L208
theorem plasmaEnergy_eq L219
theorem plasmaPressure_potential L234
theorem plasma_energyOf L255
theorem plasma_eos L265
theorem dilution_from_potential L279
theorem gStarS_from_potential L315