Theorems · Theorem · Lie groups

IsOpenUnits.of_isAdic

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] {I : Ideal R},
  IsAdic I → I ≤ ⊥.jacobson → IsOpenUnits R

If R has the I-adic topology where I is contained in the Jacobson radical (e.g. when R is complete or local), then Rˣ is an open subspace of R.

Defined in

Mathlib.Topology.Algebra.IsOpenUnits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingTopologicalSpaceIsTopologicalRing