Theorem: tangentSpace_norm_eq_complex_norm (Ray/AnalyticManifold/OneDimension.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
z : S
x : TangentSpace I z
⊢ ‖x‖ = Complex.abs x
Tactic:
rw [← Complex.norm_eq_abs]
State after:
no goals