Theorems · Definition · field theory

affineHomeomorph

{𝕜 : Type u_2} → [inst : Field 𝕜] → [inst_1 : TopologicalSpace 𝕜] → [IsTopologicalRing 𝕜] → (a : 𝕜) → 𝕜 → a ≠ 0 → 𝕜 ≃ₜ 𝕜

The map fun x => a * x + b, as a homeomorphism from 𝕜 (a topological field) to itself, when a ≠ 0.

Defined in

Mathlib.Topology.Algebra.Field

Cited by

8 results in Mathlib

Foundations

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

Assumes

FieldTopologicalSpaceIsTopologicalRing