No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
32theorem W_endo_at_3 : W_endo 3 = 17 := by native_decide
proof body
Term-mode proof.
33
34/-- W_endo(3) matches the wallpaper groups constant. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (3)
Lean names referenced from this declaration's body.
-
W_endo
in IndisputableMonolith.Masses.BaselineDerivation
decl_use
-
W_endo
in IndisputableMonolith.Physics.WEndoForcing
decl_use
-
constant
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use