Theorem Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'

Modification history

2026-09-07 13:23

Mathlib/RingTheory/Ideal/GoingUp.lean

chore(RingTheory/Ideal/GoingUp): use `Ideal.under` (#43414) …

Deleted Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'View on Github →

2025-02-07 16:33

Mathlib/RingTheory/Ideal/GoingUp.lean

chore(RingTheory/Ideal/Over): factor going-up results out (#21497) …

Modified Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'View on Github →

2023-05-23 13:58

Mathlib/RingTheory/Ideal/Over.lean

feat: port RingTheory.Ideal.Over (#4270)

Added Ideal.isMaximal_of_isIntegral_of_isMaximal_comap'View on Github →