def definition def or abbrev

`df2_dm_ratio`

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

formal statement (Lean)

  72noncomputable def df2_dm_ratio : ℝ := 1.5

Definition body.

  73
  74/-- Typical UDG surface brightness (mag/arcsec²).
  75    Value: μ_V > 24 -/

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

ngc1052df2_dm_poor in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
no_universal_ratio in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
standard_models_challenged in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use
udg_diversity_real in IndisputableMonolith.Experimental.UltraDiffuseGalaxies decl_use