Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-18 05:44 f3d3d046

View on Github →

chore(category_theory/monad): golf and lint monadic adjunctions (#5769) Some lintfixes and proof golfing using newer API

Estimated changes

Modified src/category_theory/monad/adjunction.lean

deleted theorem category_theory.adjunction.monad_η_app

deleted theorem category_theory.adjunction.monad_μ_app

modified def category_theory.monad.comparison

modified def category_theory.monad.comparison_forget

deleted theorem category_theory.monad.comparison_map_f

deleted theorem category_theory.monad.comparison_obj_a

modified theorem category_theory.reflective.comparison_ess_surj_aux