pith. machine review for the scientific record. sign in
theorem proved tactic proof

finCost_symm

show as:
view Lean formalization →

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)

  24theorem finCost_symm {m : ℕ} (x y : Fin m) : finCost x y = finCost y x := by

proof body

Tactic-mode proof.

  25  by_cases h : x = y
  26  · subst h
  27    simp [finCost]
  28  · have h' : y ≠ x := by intro hyx; exact h hyx.symm
  29    simp [finCost, h, h']
  30
  31/-- The cyclic carrier size for the `k`th modular realization. -/

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.