theorem other other

`add_zero`

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

formal statement (Lean)

 136@[simp] theorem add_zero (n : LogicNat) : n + zero = n := rfl

proof body

used by (40)

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

plot_composition_cancels_iff in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
sub_eq_add in IndisputableMonolith.Algebra.F2Power decl_use
PhiInt in IndisputableMonolith.Algebra.PhiRing decl_use
canonicalPhiRingObj in IndisputableMonolith.Algebra.RecognitionCategory decl_use
PhiRingObj in IndisputableMonolith.Algebra.RecognitionCategory decl_use
resonance_increases_stability in IndisputableMonolith.Applied.CoherenceTechnology decl_use
phi_pow_fib in IndisputableMonolith.Cosmology.EtaBPrefactorDerivation decl_use
flat_minimizes_cost in IndisputableMonolith.Cosmology.FlatnessProblem decl_use
homogeneous_minimizes_cost in IndisputableMonolith.Cosmology.HorizonProblem decl_use
phi_pow_fib_succ in IndisputableMonolith.Cosmology.MatterAntimatter decl_use
dAlembert_to_ODE_general_theorem in IndisputableMonolith.Cost.FunctionalEquation decl_use
dAlembert_to_ODE_theorem in IndisputableMonolith.Cost.FunctionalEquation decl_use
dAlembert_to_ODE_theorem in IndisputableMonolith.Cost.FunctionalEquationAczel decl_use
aggCoeff_flatMap in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
add_comm in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
embed_add in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
le_refl in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
le_succ in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
mul_add in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
one_mul in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_add in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
Composition_Normalization_implies_symmetry in IndisputableMonolith.Foundation.CostAxioms decl_use
Q_boundary_v in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
no_degree3_composition in IndisputableMonolith.Foundation.DAlembert.DegreeExclusion decl_use
dalembert_deriv_ode in IndisputableMonolith.Foundation.DAlembert.FourthGate decl_use
bilinear_family_forced in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
fromInt_toInt in IndisputableMonolith.Foundation.IntegersFromLogic decl_use
composition_consistency_not_definitional in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
regge_sum_append_trivial in IndisputableMonolith.Foundation.SimplicialLedger.CubicSimplicialEquivalence decl_use
acoustic_levitation in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use