SchemeTheory.exists_regular_pair_of_two_le_depth
Depth at least two supplies two elements of the maximal ideal that are regular in either order.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open RingTheory IsLocalRing
namespace SchemeTheoryLean source · statement
theorem exists_regular_pair_of_two_le_depth
(R : Type*) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
(hdepth : (2 : ℕ∞) ≤ Module.depth R R) :
∃ x ∈ maximalIdeal R, ∃ y ∈ maximalIdeal R,
Sequence.IsWeaklyRegular R [x, y] ∧ Sequence.IsWeaklyRegular R [y, x]