lemma
proved
wrapper
torsion_diff_21
show as:
view Lean formalization →
formal statement (Lean)
76@[simp] lemma torsion_diff_21 : torsionDiff .second .first = 11 := by
proof body
One-line wrapper that applies simp.
77 simp [torsionDiff]
78