Commit 2026-03-15 23:11 a944b6c7

View on Github →

chore(CategoryTheory/NatIso): use to_dual (#36577) This PR uses to_dual on the basic theorems about natural isomorphisms.

Estimated changes

Modified Mathlib/CategoryTheory/Iso.lean

added theorem CategoryTheory.IsIso.mk'

Modified Mathlib/CategoryTheory/NatIso.lean

modified theorem CategoryTheory.NatIso.cancel_natIso_hom_left

deleted theorem CategoryTheory.NatIso.cancel_natIso_hom_right

modified theorem CategoryTheory.NatIso.cancel_natIso_inv_left

deleted theorem CategoryTheory.NatIso.cancel_natIso_inv_right