0

合計内の if ステートメントに問題があります。

isabelle の if ステートメントに関する別の質問で解決策を確認しました が、役に立ちませんでした。

次に例を示します。

theorem dummy:
  fixes a :: "('a::comm_ring_1 poly)" 
    and B :: "(('a::comm_ring_1 poly)^'n∷finite^'n∷finite)"
  shows "1=1"
proof-
  { fix i j
   have "(∑k∈UNIV. if i = k then (B $ i $ j) else 0) = B $ i $ j" sorry
  }

「申し訳ありません」がどこにある補題をどのように証明できますか?

4

1 に答える 1