mathlib3
chore(ring_theory/algebra): add docstring to algebra.comap and remove unused instances
#1624
Merged
Overview
Commits
2
Changes
View On GitHub

chore(ring_theory/algebra): add docstring to algebra.comap and remove unused instances #1624

mergify merged 2 commits into master from ChrisHughes24-patch-2
ChrisHughes24
ChrisHughes24 doc(ring_theory/algebra): add docstring to algebra.comap
9bce0616
robertylewis
robertylewis commented on 2019-10-28
kim-em
ChrisHughes24 Update algebra.lean
eee31219
ChrisHughes24 ChrisHughes24 changed the title doc(ring_theory/algebra): add docstring to algebra.comap chore(ring_theory/algebra): add docstring to algebra.comap and remove unused instances 6 years ago
robertylewis
robertylewis approved these changes on 2019-10-28
robertylewis robertylewis added ready-to-merge
mergify mergify merged 94e368c5 into master 6 years ago
mergify mergify deleted the ChrisHughes24-patch-2 branch 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum