mathlibdocumentation

topology.algebra.field

A topological field is usually described via {𝕜 : Type*} [field 𝕜] [topological_space 𝕜] [topological_ring 𝕜] [has_continuous_inv 𝕜].

The only construction in this file doesn't need to assume [has_continuous_inv 𝕜].

def affine_homeomorph {𝕜 : Type u_1} [field 𝕜] (a b : 𝕜) (h : a 0) :
𝕜 ≃ₜ 𝕜

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

Equations
@[simp]
theorem affine_homeomorph_apply {𝕜 : Type u_1} [field 𝕜] (a b : 𝕜) (h : a 0) (x : 𝕜) :
h) x = a * x + b
@[simp]
theorem affine_homeomorph_symm_apply {𝕜 : Type u_1} [field 𝕜] (a b : 𝕜) (h : a 0) (y : 𝕜) :
b h).symm) y = (y - b) / a