structure definition def or abbrev

`ILGParams`

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

formal statement (Lean)

  44structure ILGParams where
  45  alpha : ℝ
  46  cLag  : ℝ
  47  deriving Inhabited
  48
  49/-- Index conventions (symbolic): use natural numbers as abstract tensor indices. -/

used by (13)

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

bandsFromParams in IndisputableMonolith.Relativity.ILG.Action decl_use
L_coupling in IndisputableMonolith.Relativity.ILG.Action decl_use
L_cov in IndisputableMonolith.Relativity.ILG.Action decl_use
L_density in IndisputableMonolith.Relativity.ILG.Action decl_use
L_kin in IndisputableMonolith.Relativity.ILG.Action decl_use
L_mass in IndisputableMonolith.Relativity.ILG.Action decl_use
L_pot in IndisputableMonolith.Relativity.ILG.Action decl_use
PsiActionP in IndisputableMonolith.Relativity.ILG.Action decl_use
S_on in IndisputableMonolith.Relativity.ILG.Action decl_use
S_total in IndisputableMonolith.Relativity.ILG.Action decl_use
S_total_cov in IndisputableMonolith.Relativity.ILG.Action decl_use
beta_pot in IndisputableMonolith.Relativity.ILG.PPN decl_use
gamma_pot in IndisputableMonolith.Relativity.ILG.PPN decl_use

depends on (4)

Lean names referenced from this declaration's body.

Index in IndisputableMonolith.Chemistry.PeriodicTable decl_use
alpha in IndisputableMonolith.Constants.Alpha decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
Index in IndisputableMonolith.Relativity.ILG.Action decl_use