structure definition def or abbrev

`ScaleFactor`

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

formal statement (Lean)

  12structure ScaleFactor where
  13  a : ℝ → ℝ
  14  a_positive : ∀ t, 0 < a t
  15

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

christoffel_FRW in IndisputableMonolith.Relativity.Cosmology.FRWMetric decl_use
metric_FRW in IndisputableMonolith.Relativity.Cosmology.FRWMetric decl_use
ricci_FRW_00 in IndisputableMonolith.Relativity.Cosmology.FRWMetric decl_use
ricci_FRW_ij in IndisputableMonolith.Relativity.Cosmology.FRWMetric decl_use
action_form_verified in IndisputableMonolith.Relativity.GW.ActionExpansion decl_use
action_quadratic_tensor in IndisputableMonolith.Relativity.GW.ActionExpansion decl_use
expand_action_around_FRW in IndisputableMonolith.Relativity.GW.ActionExpansion decl_use
gradient_coefficient in IndisputableMonolith.Relativity.GW.ActionExpansion decl_use
isolate_tensor_contribution in IndisputableMonolith.Relativity.GW.ActionExpansion decl_use
kinetic_coefficient in IndisputableMonolith.Relativity.GW.ActionExpansion decl_use