Skip to content

chore: remove upstreamed lemma isOpen_maximalIdeal_pow#864

Merged
kbuzzard merged 1 commit intoImperialCollegeLondon:mainfrom
dwrensha:isOpen_maximalIdeal_pow
Feb 26, 2026
Merged

chore: remove upstreamed lemma isOpen_maximalIdeal_pow#864
kbuzzard merged 1 commit intoImperialCollegeLondon:mainfrom
dwrensha:isOpen_maximalIdeal_pow

Conversation

@dwrensha
Copy link
Contributor

Removes IsLocalRing.isOpen_maximalIdeal_pow', which was added upstream as IsLocalRing.isOpen_maximalIdeal_pow in leanprover-community/mathlib4#23757.

The type of the upstream version differs only in the order of its typeclass paramters:

#check isOpen_maximalIdeal_pow
/-
IsLocalRing.isOpen_maximalIdeal_pow'.{u_1} (R : Type u_1) [CommRing R] [IsLocalRing R]
 [TopologicalSpace R] [IsTopologicalRing R] [IsNoetherianRing R] [CompactSpace R] [T2Space R]
 (n : ℕ) : IsOpen ↑(maximalIdeal R ^ n)
-/

#check isOpen_maximalIdeal_pow'
/-
IsLocalRing.isOpen_maximalIdeal_pow.{u_1} (R : Type u_1) [CommRing R] [TopologicalSpace R]
  [IsTopologicalRing R] [CompactSpace R] [T2Space R] [IsLocalRing R] [IsNoetherianRing R]
  (n : ℕ) : IsOpen ↑(maximalIdeal R ^ n)
-/

@kbuzzard kbuzzard merged commit e96749f into ImperialCollegeLondon:main Feb 26, 2026
2 checks passed
@kbuzzard
Copy link
Collaborator

Thanks!

@dwrensha dwrensha deleted the isOpen_maximalIdeal_pow branch February 26, 2026 17:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants