Theorem RingHom.injective_codRestrict

Modification history

2025-11-26 15:01

Mathlib/Algebra/Ring/Subsemiring/Basic.lean

feat(RingTheory/Congruence/Hom): prove basic isomorphisms theorems for ring congruences (#26277) …

Added RingHom.injective_codRestrict View on Github →