OAI/CategoryTheory/ThickClosure/LocalizationHom.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.HahnWilson.LocalizationHom.map_bijective_of_invertsline 14 - theorem
OAI.HahnWilson.LocalizationHom.map_bijectiveline 59