mathlib3
feat(natural_isomorphism): componentwise isos are isos
#671

Merged

feat(natural_isomorphism): componentwise isos are isos #671

rwbarton merged 3 commits into master from natural-isomorphism

feat(natural_isomorphism): instance showing a natural transformation is

02f71864

cipher1024 assigned

rwbarton 7 years ago

ensure definitional equality

7e0bedd3

define nat_iso.of_components in terms of is_iso_of_is_iso_app

f21a21cb

rwbarton merged 178c09d7 into master 7 years ago

kim-em deleted the natural-isomorphism branch 7 years ago

Reviewers

No reviews

Assignees

rwbarton

Labels

None yet

Milestone

No milestone