Commit 2024-10-19 18:37 2c5ee0d7

View on Github →

feat(RingTheory/Ideal/Over): define a class for an ideal lying over an ideal (#17415) Define class of an ideal lies over an ideal.

Estimated changes

Modified Mathlib/RingTheory/FiniteType.lean

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.NoZeroSMulDivisors.iff_ker_algebraMap_eq_bot

added theorem Ideal.NoZeroSMulDivisors.ker_algebraMap_eq_bot

added theorem Ideal.NoZeroSMulDivisors.of_ker_algebraMap_eq_bot

Modified Mathlib/RingTheory/Ideal/Over.lean

added theorem Ideal.IsMaximal.of_isMaximal_liesOver

added theorem Ideal.IsMaximal.of_liesOver_isMaximal

added theorem Ideal.LiesOver.tower_bot

added theorem Ideal.LiesOver.trans

added theorem Ideal.Quotient.algebraMap_injective_of_liesOver

added theorem Ideal.mem_of_liesOver

added theorem Ideal.over_def

added theorem Ideal.under_def

added theorem Ideal.under_under

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

added theorem Algebra.IsIntegral.tower_bot

added theorem Algebra.IsIntegral.tower_top

Modified Mathlib/RingTheory/Noetherian.lean