Theorem Ideal.Quotient.algebraMap_injective_of_liesOver
Modification history
2025-02-03 14:49
Mathlib/RingTheory/Ideal/Over.lean
feat: generalise `algebraMap_injective` by weakening its typeclass assumptions (#21287) …
Deleted Ideal.Quotient.algebraMap_injective_of_liesOverView on Github →