Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_hom.of_localization_span_target_iff_finite

Modification history

2022-07-27 11:14
src/ring_theory/local_properties.lean
feat(ring_theory/ring_hom/finite): Finite type is a local property (#15379)
Added ring_hom.of_localization_span_target_iff_finiteView on Github →