module module

`IndisputableMonolith.Physics.EM.PhotonEnergyFrequency`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (6)

def photonAction L30
def photonEnergy L34
def octaveAngularFreq L38
theorem photon_energy_eq_hbar_omega L43
theorem photon_octave_energy_phi L51
theorem photonEnergyCert L56