mathlib documentation

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 π•œ] [topological_space π•œ] [topological_ring π•œ] (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 π•œ] [topological_space π•œ] [topological_ring π•œ] (a b : π•œ) (h : a β‰  0) (x : π•œ) :
⇑(affine_homeomorph a b h) x = a * x + b
@[simp]
theorem affine_homeomorph_symm_apply {π•œ : Type u_1} [field π•œ] [topological_space π•œ] [topological_ring π•œ] (a b : π•œ) (h : a β‰  0) (y : π•œ) :
⇑((affine_homeomorph a b h).symm) y = (y - b) / a