Skip to main content
therefore
Sign inSign up
Open navigation

Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.

All topics

Showing 955 to 960 of 2,569 results.

Project-declaredLean 4.32.0

Is Extrema iff field Strength Matrix

Electromagnetism.ElectromagneticPotential.isExtrema_iff_fieldStrengthMatrix

Project documentation

The condition on an electromagnetic potential to be an extrema of the lagrangian. -/ def IsExtrema {d} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : Prop := gradLagrangian 𝓕 A J = 0 lemma isExtrema_iff_gradLagrangian {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : IsExtrema 𝓕 A J ↔ A....

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Is Extrema iff gauss ampere magnetic Field Matrix

Electromagnetism.ElectromagneticPotential.isExtrema_iff_gauss_ampere_magneticFieldMatrix

Project documentation

The condition on an electromagnetic potential to be an extrema of the lagrangian. -/ def IsExtrema {d} (𝓕 : FreeSpace) (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : Prop := gradLagrangian 𝓕 A J = 0 lemma isExtrema_iff_gradLagrangian {𝓕 : FreeSpace} (A : ElectromagneticPotential d) (J : LorentzCurrentDensity d) : IsExtrema 𝓕 A J ↔ A....

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Electric Field eq propogator cross magnetic Field Matrix

Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_eq_propogator_cross_magneticFieldMatrix

Project documentation

The corresponding magnetic field function from ℝ to Fin d Γ— Fin d β†’ ℝ of a plane wave. -/ noncomputable def magneticFunction {d : β„•} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Direction d} (hA : IsPlaneWave 𝓕 A s) : ℝ β†’ Fin d Γ— Fin d β†’ ℝ := Classical.choose hA.2 lemma magneticFieldMatrix_eq_magneticFunction {d : β„•} {𝓕 : FreeSpace} {A : E...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Electric Field space deriv eq time deriv

Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricField_space_deriv_eq_time_deriv

Project documentation

The corresponding magnetic field function from ℝ to Fin d Γ— Fin d β†’ ℝ of a plane wave. -/ noncomputable def magneticFunction {d : β„•} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Direction d} (hA : IsPlaneWave 𝓕 A s) : ℝ β†’ Fin d Γ— Fin d β†’ ℝ := Classical.choose hA.2 lemma magneticFieldMatrix_eq_magneticFunction {d : β„•} {𝓕 : FreeSpace} {A : E...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Electric Function differentiable

Electromagnetism.ElectromagneticPotential.IsPlaneWave.electricFunction_differentiable

Project documentation

The corresponding magnetic field function from ℝ to Fin d Γ— Fin d β†’ ℝ of a plane wave. -/ noncomputable def magneticFunction {d : β„•} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Direction d} (hA : IsPlaneWave 𝓕 A s) : ℝ β†’ Fin d Γ— Fin d β†’ ℝ := Classical.choose hA.2 lemma magneticFieldMatrix_eq_magneticFunction {d : β„•} {𝓕 : FreeSpace} {A : E...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Magnetic Field Matrix eq propogator cross electric Field

Electromagnetism.ElectromagneticPotential.IsPlaneWave.magneticFieldMatrix_eq_propogator_cross_electricField

Project documentation

The corresponding magnetic field function from ℝ to Fin d Γ— Fin d β†’ ℝ of a plane wave. -/ noncomputable def magneticFunction {d : β„•} {𝓕 : FreeSpace} {A : ElectromagneticPotential d} {s : Direction d} (hA : IsPlaneWave 𝓕 A s) : ℝ β†’ Fin d Γ— Fin d β†’ ℝ := Classical.choose hA.2 lemma magneticFieldMatrix_eq_magneticFunction {d : β„•} {𝓕 : FreeSpace} {A : E...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record