theorem
other
other
not_1_2_signature
show as:
view Lean formalization →
formal statement (Lean)
324theorem not_1_2_signature : ¬(spatial_dim = 2) := by simp [spatial_dim, D_physical]