165theorem wallpaperJ_pos_of_ne_one {g : WallpaperGroup} 166 (h : symmetryRatio g ≠ 1) : 0 < wallpaperJ g := by
proof body
Tactic-mode proof.
167 unfold wallpaperJ 168 have hx_pos : 0 < symmetryRatio g := symmetryRatio_pos g 169 have hx_ne : symmetryRatio g ≠ 0 := ne_of_gt hx_pos 170 rw [Cost.Jcost_eq_sq hx_ne] 171 have h_sq_pos : 0 < (symmetryRatio g - 1) ^ 2 := by 172 have h_diff : symmetryRatio g - 1 ≠ 0 := sub_ne_zero.mpr h 173 positivity 174 have h_den_pos : 0 < 2 * symmetryRatio g := by linarith 175 positivity 176 177/-- The trivial-symmetry group `p1` has strictly positive J-cost. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.