theorem other other

`mul_def`

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

formal statement (Lean)

 177@[simp] theorem mul_def (n m : LogicNat) : n * m = mul n m := rfl

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

bet1_boundaryTerm_integrable_of_L2_mul_r in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
sobolev_H1_half_line_decay in IndisputableMonolith.NavierStokes.RM2U.TailFluxInstantiation decl_use
integral_Ioi_radial_skew_identity in IndisputableMonolith.NavierStokes.SkewHarmGate decl_use
zeroSkewAtInfinity_of_integrable in IndisputableMonolith.NavierStokes.SkewHarmGate decl_use

Lean names referenced from this declaration's body.