Topological fields #
A topological division ring is a topological ring whose inversion function is continuous at every non-zero element.
Left-multiplication by a nonzero element of a topological division ring is proper, i.e., inverse images of compact sets are compact.
Right-multiplication by a nonzero element of a topological division ring is proper, i.e., inverse images of compact sets are compact.
Compact Hausdorff topological fields are finite. This is not an instance, as it would apply to
every Finite
goal, causing slowly failing typeclass search in some cases.
A topological division ring is a division ring with a topology where all operations are continuous, including inversion.
- continuous_add : Continuous fun (p : K × K) => p.1 + p.2
- continuous_mul : Continuous fun (p : K × K) => p.1 * p.2
- continuous_neg : Continuous fun (a : K) => -a
Instances
Alias of IsTopologicalDivisionRing
.
A topological division ring is a division ring with a topology where all operations are continuous, including inversion.
Instances For
The (topological-space) closure of a subfield of a topological field is itself a subfield.
Equations
- K.topologicalClosure = { carrier := closure ↑K, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, inv_mem' := ⋯ }
Instances For
This section is about affine homeomorphisms from a topological field 𝕜
to itself.
Technically it does not require 𝕜
to be a topological field, a topological ring that
happens to be a field is enough.
The map fun x => a * x + b
, as a homeomorphism from 𝕜
(a topological field) to itself,
when a ≠ 0
.
Equations
Instances For
Some results about functions on preconnected sets valued in a ring or field with a topology.
If f
is a function α → 𝕜
which is continuous on a preconnected set S
, and
f ^ 2 = 1
on S
, then either f = 1
on S
, or f = -1
on S
.
If f, g
are functions α → 𝕜
, both continuous on a preconnected set S
, with
f ^ 2 = g ^ 2
on S
, and g z ≠ 0
all z ∈ S
, then either f = g
or f = -g
on
S
.
If f, g
are functions α → 𝕜
, both continuous on a preconnected set S
, with
f ^ 2 = g ^ 2
on S
, and g z ≠ 0
all z ∈ S
, then as soon as f = g
holds at
one point of S
it holds for all points.