def definition def or abbrev

`gamma`

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

formal statement (Lean)

  14noncomputable def gamma (_C_lag _α : ℝ) : ℝ := 1

used by (40)

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

phi_fifth_in_alpha_band in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
rs_pattern_sqrt_components_neutral in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
cubicConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
hexagonalConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
LatticeParams in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
monoclinicConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
orthorhombicConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
tetragonalConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
trigonalConstraint in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
euler_mascheroni_bounds in IndisputableMonolith.Constants.EulerMascheroni decl_use
euler_mascheroni_implies_ne_zero in IndisputableMonolith.Constants.EulerMascheroni decl_use
euler_mascheroni_implies_pos in IndisputableMonolith.Constants.EulerMascheroni decl_use
gamma in IndisputableMonolith.Constants.EulerMascheroni decl_use
gamma_lt_two_thirds in IndisputableMonolith.Constants.EulerMascheroni decl_use
gamma_numerical_bounds in IndisputableMonolith.Constants.EulerMascheroni decl_use
gamma_pos in IndisputableMonolith.Constants.EulerMascheroni decl_use
coupling_from_spectral in IndisputableMonolith.Gravity.CaldeiraLeggett decl_use
ChristoffelData in IndisputableMonolith.Gravity.Connection decl_use
christoffel_from_metric in IndisputableMonolith.Gravity.Connection decl_use
christoffel_symmetric in IndisputableMonolith.Gravity.Connection decl_use
ConnectionCert in IndisputableMonolith.Gravity.Connection decl_use
flat_christoffel_vanish in IndisputableMonolith.Gravity.Connection decl_use
metric_compatibility in IndisputableMonolith.Gravity.Connection decl_use
HilbertVariationCert in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
hilbert_variation_holds in IndisputableMonolith.Gravity.EinsteinHilbertAction decl_use
einstein_symmetric in IndisputableMonolith.Gravity.RicciTensor decl_use
einstein_tensor in IndisputableMonolith.Gravity.RicciTensor decl_use
ricci_tensor in IndisputableMonolith.Gravity.RicciTensor decl_use
scalar_curvature in IndisputableMonolith.Gravity.RicciTensor decl_use
sourced_efe_coord in IndisputableMonolith.Gravity.RicciTensor decl_use

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.

gamma in IndisputableMonolith.Constants.EulerMascheroni decl_use
gamma in IndisputableMonolith.NetworkScience.SmallWorldFromSigma decl_use