abbrev definition def or abbrev

`Tensor`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  12abbrev Tensor (p q : ℕ) := (Fin 4 → ℝ) → (Fin p → Fin 4) → (Fin q → Fin 4) → ℝ

proof body

Definition body.

used by (25)

From the project-wide theorem graph. These declarations reference this one in their body.

experimentalStatus in IndisputableMonolith.Cosmology.Inflation decl_use
InflationPredictions in IndisputableMonolith.Cosmology.Inflation decl_use
tensorScalarRatio in IndisputableMonolith.Cosmology.Inflation decl_use
amplitude_derivation in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
TotalHamiltonian in IndisputableMonolith.Foundation.Hamiltonian decl_use
Idx in IndisputableMonolith.Gravity.Connection decl_use
spectral_index in IndisputableMonolith.Gravity.Inflation decl_use
scalar_flat in IndisputableMonolith.Gravity.RicciTensor decl_use
experimentalStatus in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
experimentalTests in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
implications in IndisputableMonolith.Quantum.EntanglementEntropy decl_use
christoffel_symmetric in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
ricci_scalar in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
riemann_tensor in IndisputableMonolith.Relativity.Geometry.Curvature decl_use
riemann_pair_exchange_proof in IndisputableMonolith.Relativity.Geometry.RiemannSymmetries decl_use
antisymmetrize in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
BilinearForm in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
contract in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
ContravariantBilinear in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
CovectorField in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
IsSymmetric in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
symmetrize in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
tensor_product in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
VectorField in IndisputableMonolith.Relativity.Geometry.Tensor decl_use
zero_tensor in IndisputableMonolith.Relativity.Geometry.Tensor decl_use