Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2023-01-22 11:32
fc3dc609
View on Github →
chore(order/filter/basic): fix 2 typos (
#18253
)
Estimated changes
Modified
src/order/filter/basic.lean
deleted
theorem
commute.filter_comap
deleted
theorem
commute.filter_map
added
theorem
function.commute.filter_comap
added
theorem
function.commute.filter_map