2024年5月7日

昨日の関数合成はなんか違ったかも…….でもよくわかってない.

import Mathlib.Tactic
open Nat

@[simp]
def fun_pow {α : Type u} (f : α → α) : (n : Nat) → (α → α)
  | 0 => id
  | succ n => (fun_pow f n) ∘ f

instance {α : Type u} : HPow (α → α) (Nat) (α → α) where
  hPow := fun_pow

def f : (Fin 2) → (Fin 2)
  | 0 => 1
  | 1 => 0

theorem a {α : Type u} (g : α → α) : g^(0) = id := by rfl
theorem aa : f^(0) = id := by
  rfl

最後のrflが通らない.simpすると1 = idとかに簡略化されてしまっているらしい.何だろう.うーむ.最初のimportがないと動くような.

0 件のコメント:

コメントを投稿

コメントの追加にはサードパーティーCookieの許可が必要です