Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-10-15 10:28
bfa61d17
View on Github →
chore: rename IrreducibleCloseds fields to match naming convention (
#30550
)
Estimated changes
Modified
Mathlib/Topology/KrullDimension.lean
Modified
Mathlib/Topology/Sets/Closeds.lean
modified
theorem
TopologicalSpace.IrreducibleCloseds.isClosed
modified
theorem
TopologicalSpace.IrreducibleCloseds.isIrreducible