index
:
aoc-2023
feature/day17
main
Advent of Code 2023 - I'm still learning Lean4, so please don't judge.
Andreas Grois
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
Common
/
Function.lean
blob: 691a0686bd2db4abfcb35e1b548f7ebbb9e38b52 (
plain
) (
blame
)
1
theorem
Function
.
comp_assoc
(
f
:
γ
→
δ
)
(
g
:
β
→
γ
)
(
h
:
α
→
β
)
:
(
f
∘
g
)
∘
h
=
f
∘
g
∘
h
:=
rfl