Source-pinned research
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.
Showing 1,639 to 1,644 of 2,569 results.
Lorentz.CoMod.stdBasis_decomp
Mathematical statement
Decomposition of a covariant Lorentz vector into the standard basis.
Source project: Physlib
Person-level attribution pending.
Lorentz.contr_coContrUnit
Mathematical statement
Contraction on the right with coContrUnit.
Source project: Physlib
Person-level attribution pending.
Lorentz.contr_preCoContrUnit
Mathematical statement
Contraction on the right with coContrUnit.
Source project: Physlib
Person-level attribution pending.
Lorentz.contr_preContrCoUnit
Mathematical statement
Contraction on the right with contrCoUnit does nothing.
Source project: Physlib
Person-level attribution pending.
Lorentz.contrCoContraction_apply_metric
Project documentation
The metric ηᵢᵢ as a morphism 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexCo ⊗ complexCo, making its invariance under the action of SL(2,ℂ). -/ def coMetric : (Representation.trivial ℂ SL(2,ℂ) ℂ).IntertwiningMap (CoℂModule.SL2CRep.tprod CoℂModule.SL2CRep) where toFun := fun a => let a' : ℂ := a a' • coMetricVal map_add' := fun x y => by simp only [add_smul] map_smu...
Source project: Physlib
Person-level attribution pending.
Lorentz.contrContrContractField.basis_left
Project documentation
The metric tensor is non-degenerate. -/ lemma nondegenerate : (∀ (x : ContrMod d), ⟪x, y⟫ₘ = 0) ↔ y = 0 := by refine Iff.intro (fun h => ?) (fun h => ?) · exact (self_parity_eq_zero_iff _).mp ((symm _ _).trans $ h _) · simp [h] set_option backward.isDefEq.respectTransparency false in lemma matrix_apply_eq_iff_sub : ⟪x, Λ *ᵥ y⟫ₘ = ⟪x, Λ' *ᵥ y⟫ₘ ↔ ⟪x, (Λ...
Source project: Physlib
Person-level attribution pending.