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

1 topic

9 results

Clear filters
Project-declaredLean 4.32.0

Magnetic Field Matrix space deriv eq

Electromagnetism.ElectromagneticPotential.magneticFieldMatrix_space_deriv_eq

Project documentation

The matrix corresponding to the magnetic field in general dimensions. In 3 space-dimensions this reduces to a vector. -/ noncomputable def magneticFieldMatrix (c : SpeedOfLight := 1) (A : ElectromagneticPotential d) : Time → Space d → (Fin d × Fin d) → ℝ := timeSlice c <| fun x ij => A.fieldStrengthMatrix x (Sum.inr ij.1, Sum.inr ij.2) lemma magneticFie...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Of Electromagnetic Field magnetic Field

Electromagnetism.ElectromagneticPotential.ofElectromagneticField_magneticField

Plain-language statement

The magnetic field of the electromagnetic potential created from the electric field E and the magnetic field B is B, as long as Gauss's law is satisfied.

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Time deriv magnetic Field Matrix

Electromagnetism.ElectromagneticPotential.time_deriv_magneticFieldMatrix

Project documentation

The matrix corresponding to the magnetic field in general dimensions. In 3 space-dimensions this reduces to a vector. -/ noncomputable def magneticFieldMatrix (c : SpeedOfLight := 1) (A : ElectromagneticPotential d) : Time → Space d → (Fin d × Fin d) → ℝ := timeSlice c <| fun x ij => A.fieldStrengthMatrix x (Sum.inr ij.1, Sum.inr ij.2) lemma magneticFie...

physicsquantum field theoryrelativity

Source project: Physlib

Person-level attribution pending.

View proof record