Def CategoryTheory.Functor.autMulEquivOfFullyFaithful

Modification history

2024-04-27 09:23

Mathlib/CategoryTheory/Endomorphism.lean

chore(CategoryTheory): make `Functor.Full` a Prop (#12449) …

Deleted CategoryTheory.Functor.autMulEquivOfFullyFaithful View on Github →

2024-01-09 08:14

Mathlib/CategoryTheory/Endomorphism.lean

feat: add multiplicative versions of `equivOfFullyFaithful` and `isoEquivOfFullyFaithful` (#9566) …

Added CategoryTheory.Functor.autMulEquivOfFullyFaithful View on Github →