Theorems · Theorem · ring theory

IsArtinianRing.finite_of_compactSpace_of_t2Space

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [IsArtinianRing R], Finite R

Compact Hausdorff Artinian (commutative) rings are finite. This is not an instance, as it would apply to every Finite goal, causing slowly failing typeclass search in some cases.

Defined in

Mathlib.Topology.Algebra.Ring.Compact

Cited by

0 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingTopologicalSpaceIsTopologicalRingCompactSpaceT2SpaceIsArtinianRing