Option map of some
Closed
Theorem & proof
·
option_map_some.lean
·
✓ verified
1
2
3
import Mathlib theorem option_map_some {α β : Type} (f : α → β) (a : α) : (Option.some a).map f = Option.some (f a) :=rfl
Rewards pledged
No rewards pledged yet.