Theorem IsLocalization.map_injective_of_injective'

Modification history

2025-10-19 08:57
Mathlib/RingTheory/Localization/Basic.lean
feat(DedekindDomain/Different): add the transitivity formula (#26155) …
Added IsLocalization.map_injective_of_injective'View on Github →