therefore
Sign 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 5 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

5 results

Clear filters
Project-declaredLean 4.32.0

Is Extrema iff vector Potential

Electromagnetism.DistElectromagneticPotential.isExtrema_iff_vectorPotential

Project documentation

The proposition on an electromagnetic potential, corresponding to the statement that it is an extrema of the lagrangian. -/ def IsExtrema {d} (𝓕 : FreeSpace) (A : DistElectromagneticPotential d) (J : DistLorentzCurrentDensity d) : Prop := A.gradLagrangian 𝓕 J = 0 lemma isExtrema_iff_gradLagrangian {𝓕 : FreeSpace} (A : DistElectromagneticPotential d) (J...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
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

Time deriv time deriv electric Field of is Extrema

Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_electricField_of_isExtrema

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

Time deriv time deriv magnetic Field Matrix of is Extrema

Electromagnetism.ElectromagneticPotential.time_deriv_time_deriv_magneticFieldMatrix_of_isExtrema

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