def definition def or abbrev

`T`

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

formal statement (Lean)

  38def T (n : ℕ) : ℕ := n * (n + 1) / 2

proof body

Definition body.

used by (40)

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

space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
Jcost_quadratic_leading_coeff in IndisputableMonolith.Action.QuadraticLimit decl_use
newton_first_law in IndisputableMonolith.Action.QuadraticLimit decl_use
narrativeGeodesicCert in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
arrheniusRate in IndisputableMonolith.Chemistry.ActivationEnergy decl_use
higher_barrier_slower in IndisputableMonolith.Chemistry.ActivationEnergy decl_use
co_high_anisotropy in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
magnetizationRatio in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
nonzero_below_curie in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
zero_above_curie in IndisputableMonolith.Chemistry.Ferromagnetism decl_use
HaberBoschCert in IndisputableMonolith.Chemistry.HaberBoschFromPhiLadder decl_use
haberBoschTempCost_at_min in IndisputableMonolith.Chemistry.HaberBoschFromPhiLadder decl_use
transition_cohesive_gt_alkali in IndisputableMonolith.Chemistry.MetallicBond decl_use
H_SATTMRuntime in IndisputableMonolith.Complexity.CellularAutomata decl_use
main_resolution in IndisputableMonolith.Complexity.ComputationBridge decl_use
TuringModel in IndisputableMonolith.Complexity.ComputationBridge decl_use
caTimeBound in IndisputableMonolith.Complexity.SAT.Runtime decl_use
C006_certificate in IndisputableMonolith.Constants.BoltzmannConstant decl_use
k_R_eq_J_bit in IndisputableMonolith.Constants.BoltzmannConstant decl_use
thermal_energy_at_unit_T in IndisputableMonolith.Constants.BoltzmannConstant decl_use
Dimension in IndisputableMonolith.Constants.Dimensions decl_use
DimensionedQuantity in IndisputableMonolith.Constants.Dimensions decl_use
DimensionedQuantity in IndisputableMonolith.Constants.Dimensions decl_use
DimensionedQuantity in IndisputableMonolith.Constants.Dimensions decl_use
dimensions_status in IndisputableMonolith.Constants.Dimensions decl_use
dim_G in IndisputableMonolith.Constants.Dimensions decl_use
number_of_patches in IndisputableMonolith.Cosmology.HorizonProblem decl_use
both_predictions_match in IndisputableMonolith.Cosmology.HubbleTensionCertificate decl_use
dual_metric_structural in IndisputableMonolith.Cosmology.HubbleTensionCertificate decl_use
H_late_precision_bounds in IndisputableMonolith.Cosmology.HubbleTensionCertificate decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

T in IndisputableMonolith.Foundation.Breath1024 decl_use