apply(Lean)
#Fleeting_Notes
apply(Lean)
apply?
現在のゴールに適用可能なmathlibの定理(もしくは定義)を探すタクティク
code:lean
example
Group G
Group H
(f : G →* H) (a b : G) :
f (a * b) = f a * f b := by
-- ヒント:
apply?
を使う
--
apply?
を使うと「Try this: exact MonoidHom.map_mul f a b」というメッセージが出る(!!)
exact MonoidHom.map_mul f a b
確認用
Q. apply(Lean)
参考
調査用
Google.icon
apply Lean(日)
Google.icon
apply Lean(英)