mathlib documentation

algebra.category.CommRing.instances

Ring-theoretic results in terms of categorical languages #

source
@[protected, instance]
def localization_unit_is_iso (R : CommRing) :
category_theory.is_iso (CommRing.of_hom (algebra_map ↥R (localization.away 1)))
source
@[protected, instance]
def localization_unit_is_iso' (R : CommRing) :
category_theory.is_iso (CommRing.of_hom (algebra_map ↥R (localization.away 1)))