Theorem CategoryTheory.ConcreteCategory.isIso_iff_bijective

Modification history

2024-06-13 19:34
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
chore: move material on limits out of ConcreteCategory.Basic (#13549) …
Modified CategoryTheory.ConcreteCategory.isIso_iff_bijectiveView on Github →
2024-04-12 14:33
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
chore(CategoryTheory): move Full, Faithful, EssSurj, IsEquivalence and ReflectsIsomorphisms to the Functor namespace (#11985) …
Modified CategoryTheory.ConcreteCategory.isIso_iff_bijectiveView on Github →
2024-02-08 20:07
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
feat(CategoryTheory/Galois): characterisation of connected finite `G`-sets (#10228) …
Added CategoryTheory.ConcreteCategory.isIso_iff_bijectiveView on Github →