case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type ?u.124862
M' : Type ?u.124865
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
g : N →L[R] G
c✝ c : R
hc : c ≠ 0
c' : R
hc' : c' ≠ 0
li : M →ₗᵢ[R] N
⊢ IsConformalMap (c • c' • toContinuousLinearMap li)
R : Type u_1
M : Type u_2
N : Type u_3
G : Type ?u.124862
M' : Type ?u.124865
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
f : M →L[R] N
g : N →L[R] G
c✝ : R
hf : IsConformalMap f
c : R
hc : c ≠ 0
⊢ IsConformalMap (c • f)
rcases hf with ⟨c', hc', li, rfl⟩
no goals
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
G : Type ?u.124862
M' : Type ?u.124865
inst✝⁸ : NormedField R
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
inst✝⁵ : SeminormedAddCommGroup G
inst✝⁴ : NormedSpace R M
inst✝³ : NormedSpace R N
inst✝² : NormedSpace R G
inst✝¹ : NormedAddCommGroup M'
inst✝ : NormedSpace R M'
g : N →L[R] G
c✝ c : R
hc : c ≠ 0
c' : R
hc' : c' ≠ 0
li : M →ₗᵢ[R] N
⊢ IsConformalMap (c • c' • toContinuousLinearMap li)
exact ⟨c * c', mul_ne_zero hc hc', li, smul_smul _ _ _⟩