Project-declaredLean 4.32.0
Time deriv curl commute
Space.time_deriv_curl_commute
Plain-language statement
Curl and time derivative commute.
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersView proof record
Project-declaredLean 4.32.0
Det time Space Basis Equiv
SpaceTime.det_timeSpaceBasisEquiv
Project documentation
The equivalence on of SpaceTime taking (1, 0, 0, ...) to of (c, 0, 0, ....) and keeping all other components the same. -/ def timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) : SpaceTime d ≃L[ℝ] SpaceTime d where toFun x := fun μ => match μ with | Sum.inl 0 => c.val * x (Sum.inl 0) | Sum.inr i => x (Sum.inr i) invFun x := fun μ => match μ with | Sum.i...
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Space Time integral eq time space integral
SpaceTime.spaceTime_integral_eq_time_space_integral
Project documentation
The equivalence on of SpaceTime taking (1, 0, 0, ...) to of (c, 0, 0, ....) and keeping all other components the same. -/ def timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) : SpaceTime d ≃L[ℝ] SpaceTime d where toFun x := fun μ => match μ with | Sum.inl 0 => c.val * x (Sum.inl 0) | Sum.inr i => x (Sum.inr i) invFun x := fun μ => match μ with | Sum.i...
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Time Space Basis add Haar
SpaceTime.timeSpaceBasis_addHaar
Project documentation
The equivalence on of SpaceTime taking (1, 0, 0, ...) to of (c, 0, 0, ....) and keeping all other components the same. -/ def timeSpaceBasisEquiv {d : ℕ} (c : SpeedOfLight) : SpaceTime d ≃L[ℝ] SpaceTime d where toFun x := fun μ => match μ with | Sum.inl 0 => c.val * x (Sum.inl 0) | Sum.inr i => x (Sum.inr i) invFun x := fun μ => match μ with | Sum.i...
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Of U1Subgroup smul eq smul
StandardModel.HiggsVec.ofU1Subgroup_smul_eq_smul
Project documentation
The subgroup of gaugeGroup := SU(3) × SU(2) × U(1) which preserves every HiggsVec by the action of StandardModel.HiggsVec.rep is given by SU(3) × ℤ₆ where ℤ₆ is the subgroup of SU(2) × U(1) with elements (α^(-3) * I₂, α) where α is a sixth root of unity. -/ informal_lemma stability_group where deps := [``HiggsVec] tag := "6V2MO" /-! ## A.8...
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.
Project-declaredLean 4.32.0
Cross product t
standParam.cross_product_t
Plain-language statement
The top-row of the standard parameterization is the cross product of the conjugate of the up and charm rows.
physicsquantum field theoryrelativity
Source project: Physlib
Person-level attribution pending.