Theorem Ideal.NoZeroSMulDivisors.ker_algebraMap_eq_bot

Modification history

2025-02-03 14:49
Mathlib/RingTheory/Ideal/Maps.lean
feat: generalise `algebraMap_injective` by weakening its typeclass assumptions (#21287) …
Deleted Ideal.NoZeroSMulDivisors.ker_algebraMap_eq_botView on Github →
2025-01-07 20:33
Mathlib/RingTheory/Ideal/Maps.lean
chore(Noetherian/Artinian): generalize to Semiring (#20534)
Modified Ideal.NoZeroSMulDivisors.ker_algebraMap_eq_botView on Github →
2024-10-19 18:37
Mathlib/RingTheory/Ideal/Maps.lean
feat(RingTheory/Ideal/Over): define a class for an ideal lying over an ideal (#17415) …
Added Ideal.NoZeroSMulDivisors.ker_algebraMap_eq_botView on Github →