mathlib3 documentation

analysis.normed_space.conformal_linear_map

Conformal Linear Maps #

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

A continuous linear map between R-normed spaces X and Y is_conformal_map if it is a nonzero multiple of a linear isometry.

Main definitions #

Main results #

See analysis.normed_space.conformal_linear_map.inner_product for

Tags #

conformal

Warning #

The definition of conformality in this file does NOT require the maps to be orientation-preserving.

def is_conformal_map {R : Type u_1} {X : Type u_2} {Y : Type u_3} [normed_field R] [seminormed_add_comm_group X] [seminormed_add_comm_group Y] [normed_space R X] [normed_space R Y] (f' : X →L[R] Y) :
Prop

A continuous linear map f' is said to be conformal if it's a nonzero multiple of a linear isometry.

Equations
theorem is_conformal_map.smul {R : Type u_1} {M : Type u_2} {N : Type u_3} [normed_field R] [seminormed_add_comm_group M] [seminormed_add_comm_group N] [normed_space R M] [normed_space R N] {f : M →L[R] N} (hf : is_conformal_map f) {c : R} (hc : c 0) :
@[protected]
theorem is_conformal_map.ne_zero {R : Type u_1} {N : Type u_3} {M' : Type u_5} [normed_field R] [seminormed_add_comm_group N] [normed_space R N] [normed_add_comm_group M'] [normed_space R M'] [nontrivial M'] {f' : M' →L[R] N} (hf' : is_conformal_map f') :
f' 0