mathlib3 documentation

geometry.manifold.conformal_groupoid

Conformal Groupoid #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define the groupoid of conformal maps on normed spaces.

Main definitions #

conformal_groupoid: the groupoid of conformal local homeomorphisms.

Tags #

conformal, groupoid

def conformal_pregroupoid {X : Type u_1} [normed_add_comm_group X] [normed_space ℝ X] :

The pregroupoid of conformal maps.

Equations

conformal_pregroupoid = {property := λ (f : X → X) (u : set X), ∀ (x : X), x ∈ u → conformal_at f x, comp := _, id_mem := _, locality := _, congr := _}

def conformal_groupoid {X : Type u_1} [normed_add_comm_group X] [normed_space ℝ X] :

structure_groupoid X

The groupoid of conformal maps.

Equations

conformal_groupoid = conformal_pregroupoid.groupoid