Def dfinsupp.zip_with
Modification history
2022-07-20 11:04
src/data/dfinsupp/basic.lean
refactor(data/dfinsupp/basic): Improve definitional equalities of coercions (#15521) …
Modified dfinsupp.zip_withView on Github →2021-09-15 13:22
src/data/dfinsupp.lean
chore(data/dfinsupp): golf using `quotient.map` instead of `quotient.lift_on` (#9176)
Modified dfinsupp.zip_withView on Github →