MinkowskiMatrix

📁 Source: PhysLean/Relativity/MinkowskiMatrix.lean

Statistics

Metric	Count
Definitions `minkowskiMatrix`, `dual`, `termη`	3
Theorems `as_block`, `as_diagonal`, `det_dual`, `det_eq_neg_one_pow_d`, `dual_apply`, `dual_apply_minkowskiMatrix`, `dual_dual`, `dual_eta`, `dual_id`, `dual_mul`, `dual_transpose`, `eq_transpose`, `inl_0_inl_0`, `inr_i_inr_i`, `mulVec_inl_0`, `mulVec_inr_i`, `mul_η_diag_eq_iff`, `off_diag_zero`, `sq`, `η_apply_mul_η_apply_diag`, `η_apply_sq_eq_one`, `η_diag_ne_zero`	22
Total	25

(root)

Definitions

Name	Category	Theorems
`minkowskiMatrix` 📖	CompOp	83 math math: `Lorentz.Vector.minkowskiProduct_basis_right`, `LorentzGroup.genBoostAux₁_basis_genBoostAux₂_minkowskiProduct`, `minkowskiMatrix.dual_eta`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_potential`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_sum_fieldStrengthMatrix`, `LorentzGroup.mul_minkowskiMatrix_mul_transpose`, `lorentzAlgebra.transpose_eq_neg_eta_conj`, `Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_tensor`, `LorentzGroup.mem_iff_transpose_mul_minkowskiMatrix_mul_self`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_sum_sum`, `minkowskiMatrix.inr_i_inr_i`, `Lorentz.contrContrContractField.basis_left`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_fieldStrength`, `Electromagnetism.ElectromagneticPotential.freeCurrentPotential_hasVarGradientAt`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_sum_sum`, `Electromagnetism.DistElectromagneticPotential.gradLagrangian_eq_tensor`, `minkowskiMatrix.inl_0_inl_0`, `Electromagnetism.ElectromagneticPotential.gradLagrangian_eq_tensor`, `realLorentzTensor.contrMetric_repr_apply_eq_minkowskiMatrix`, `Lorentz.preContrMetricVal_expand_tmul_minkowskiMatrix`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_distTensorDeriv`, `LorentzGroup.genBoostAux₁_toMatrix_apply`, `minkowskiMatrix.eq_transpose`, `minkowskiMatrix.as_block`, `lorentzAlgebra.mem_iff'`, `Electromagnetism.ElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_sum_basis`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_basis_repr_apply_eq_single`, `LorentzGroup.genearlizedBoost_apply_basis`, `Lorentz.Vector.minkowskiProduct_basis_left`, `LorentzGroup.genBoostAux₁_add_genBoostAux₂_minkowskiProduct`, `LorentzGroup.transpose_mul_minkowskiMatrix_mul_self`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_basis_repr_eq_single`, `Lorentz.contrContrContractField.on_basis`, `Electromagnetism.ElectromagneticPotential.canonicalMomentum_eq`, `realLorentzTensor.coMetric_repr_apply_eq_minkowskiMatrix`, `Lorentz.Vector.minkowskiProduct_toCoord_minkowskiMatrix`, `Electromagnetism.ElectromagneticPotential.toTensor_toFieldStrength_basis_repr`, `LorentzGroup.generalizedBoost_apply_eq_minkowskiProduct`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_fieldStrengthMatrix_sq`, `LorentzGroup.minkowskiMatrix_comm`, `minkowskiMatrix.mulVec_inl_0`, `minkowskiMatrix.as_diagonal`, `Electromagnetism.DistElectromagneticPotential.fieldStrength_eq_basis`, `lorentzAlgebra.mem_iff`, `Lorentz.contrContrContractField.matrix_apply_stdBasis`, `minkowskiMatrix.η_apply_mul_η_apply_diag`, `Lorentz.contrContrContract_hom_tmul`, `Electromagnetism.DistElectromagneticPotential.gradFreeCurrentPotential_eq_tensor`, `minkowskiMatrix.mulVec_inr_i`, `LorentzGroup.toComplex_mul_minkowskiMatrix_mul_transpose`, `minkowskiMatrix.dual_apply_minkowskiMatrix`, `minkowskiMatrix.det_eq_neg_one_pow_d`, `Electromagnetism.ElectromagneticPotential.gradKineticTerm_eq_tensorDeriv`, `Lorentz.coCoContract_hom_tmul`, `LorentzGroup.comm_minkowskiMatrix`, `PauliMatrix.pauliBasis_minkowskiMetric_pauliBasis'`, `minkowskiMatrix.mul_η_diag_eq_iff`, `minkowskiMatrix.dual_apply`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply_eq_single`, `LorentzGroup.genBoostAux₂_toMatrix_apply`, `LorentzGroup.genBoostAux₁_basis_minkowskiProduct`, `minkowskiMatrix.η_apply_sq_eq_one`, `Electromagnetism.ElectromagneticPotential.toFieldStrength_basis_repr_apply`, `Electromagnetism.ElectromagneticPotential.kineticTerm_eq_sum_fieldStrengthMatrix`, `LorentzGroup.generalizedBoost_apply_eq_toCoord`, `Electromagnetism.ElectromagneticPotential.kineticTerm_add_time_mul_const`, `LorentzGroup.genBoostAux₂_basis_minkowskiProduct`, `lorentzAlgebra.exp_transpose_of_mem_algebra`, `Lorentz.contrContrContractField.on_basis_mulVec`, `minkowskiMatrix.sq`, `minkowskiMatrix.off_diag_zero`, `Electromagnetism.DistElectromagneticPotential.fieldStrengthAux_eq_basis`, `LorentzGroup.genBoostAux₂_apply_basis`, `LorentzGroup.genBoostAux₁_apply_basis`, `LorentzGroup.toComplex_transpose_mul_minkowskiMatrix_mul_self`, `lorentzAlgebra.transpose_eta`, `Electromagnetism.DistElectromagneticPotential.gradKineticTerm_eq_fieldStrength`, `LorentzGroup.basis_minkowskiProduct_genBoostAux₁_add_genBoostAux₂`, `Lorentz.preCoMetricVal_expand_tmul_minkowskiMatrix`, `Electromagnetism.DistElectromagneticPotential.toTensor_fieldStrengthAux_basis_repr`

minkowskiMatrix

Definitions

Name	Category	Theorems
`dual` 📖	CompOp	16 math math: `dual_eta`, `lorentzGroupIsGroup_div`, `dual_dual`, `LorentzGroup.dual_mem`, `LorentzGroup.mem_iff_self_mul_dual`, `det_dual`, `Lorentz.contrContrContractField.dual_mulVec_right`, `dual_transpose`, `dual_mul`, `dual_apply_minkowskiMatrix`, `LorentzGroup.inv_eq_dual`, `dual_apply`, `LorentzGroup.toProd_eq_transpose_η`, `Lorentz.contrContrContractField.dual_mulVec_left`, `dual_id`, `LorentzGroup.mem_iff_dual_mul_self`
`termη` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`as_block` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal`
`as_diagonal` 📖	mathematical	—	`minkowskiMatrix`	—	—
`det_dual` 📖	mathematical	—	`dual`	—	`det_eq_neg_one_pow_d`
`det_eq_neg_one_pow_d` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal`
`dual_apply` 📖	mathematical	—	`dual` `minkowskiMatrix`	—	`as_diagonal`
`dual_apply_minkowskiMatrix` 📖	mathematical	—	`dual` `minkowskiMatrix`	—	`dual_apply` `η_apply_mul_η_apply_diag`
`dual_dual` 📖	mathematical	—	`dual`	—	`eq_transpose` `sq`
`dual_eta` 📖	mathematical	—	`dual` `minkowskiMatrix`	—	`eq_transpose` `sq`
`dual_id` 📖	mathematical	—	`dual`	—	`sq`
`dual_mul` 📖	mathematical	—	`dual`	—	`sq`
`dual_transpose` 📖	mathematical	—	`dual`	—	`eq_transpose`
`eq_transpose` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal`
`inl_0_inl_0` 📖	mathematical	—	`minkowskiMatrix`	—	—
`inr_i_inr_i` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal`
`mulVec_inl_0` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal`
`mulVec_inr_i` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal`
`mul_η_diag_eq_iff` 📖	mathematical	—	`minkowskiMatrix`	—	`η_diag_ne_zero`
`off_diag_zero` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal`
`sq` 📖	mathematical	—	`minkowskiMatrix`	—	`as_block`
`η_apply_mul_η_apply_diag` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal`
`η_apply_sq_eq_one` 📖	mathematical	—	`minkowskiMatrix`	—	`as_diagonal` `inr_i_inr_i`
`η_diag_ne_zero` 📖	—	—	—	—	`as_diagonal`

---

← Back to Index