theorem other other

`mul_zero`

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

formal statement (Lean)

 179@[simp] theorem mul_zero (n : LogicNat) : n * zero = zero := rfl

proof body

used by (40)

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

newton_first_law in IndisputableMonolith.Action.QuadraticLimit decl_use
PhiInt in IndisputableMonolith.Algebra.PhiRing decl_use
PhiInt in IndisputableMonolith.Algebra.PhiRing decl_use
min_energy_zero in IndisputableMonolith.Chemistry.Quasicrystal decl_use
flat_minimizes_cost in IndisputableMonolith.Cosmology.FlatnessProblem decl_use
aux_limit_N_plus_two_div_pow in IndisputableMonolith.Decision.StPetersburg decl_use
costAlphaLog_fourth_deriv_at_zero in IndisputableMonolith.Foundation.AlphaCoordinateFixation decl_use
mul_add in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
mul_one in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
toNat_mul in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use
Composition_Normalization_implies_symmetry in IndisputableMonolith.Foundation.CostAxioms decl_use
flat_ode_unique in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
bilinear_family_forced in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
polynomial_form_forced in IndisputableMonolith.Foundation.DAlembert.Inevitability decl_use
costAlphaLog_unit_curvature in IndisputableMonolith.Foundation.DAlembert.WLOGAlphaOne decl_use
phase_0_is_one in IndisputableMonolith.Foundation.EightTick decl_use
flat_is_vacuum in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
flat_regge_sum_zero in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumTheorem decl_use
no_smaller_multiple_8_45 in IndisputableMonolith.Gap45 decl_use
no_smaller_multiple_9_5 in IndisputableMonolith.Gap45 decl_use
no_smaller_multiple_8_45 in IndisputableMonolith.Gap45.Beat decl_use
linear_regge_vanishes in IndisputableMonolith.Geometry.DeficitLinearization decl_use
acoustic_levitation in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
equilibrium_is_coherent in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
modified_falling_condition in IndisputableMonolith.Gravity.AcousticPhaseLevitation decl_use
w_at_resonance in IndisputableMonolith.Gravity.EightTickResonance decl_use
f_growth_gr_limit in IndisputableMonolith.Gravity.ILGGrowthFactor decl_use
regge_action_flat in IndisputableMonolith.Gravity.ReggeCalculus decl_use
conservation_from_efe_and_bianchi in IndisputableMonolith.Gravity.StressEnergyTensor decl_use
dirichletForm_flat in IndisputableMonolith.Gravity.WeakFieldConformalRegge decl_use

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.

LogicNat in IndisputableMonolith.Foundation.ArithmeticFromLogic decl_use