Commit 2023-08-01 10:36 bfd9478a

View on Github →

feat: products of Thunks (#6096)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/LazyList/Basic.lean

deleted theorem Thunk.ext

Modified Mathlib/Init/Core.lean

Created Mathlib/Lean/Thunk.lean

added theorem Thunk.ext

added def Thunk.prod

added theorem Thunk.prod_get_fst

added theorem Thunk.prod_get_snd