`BookProof.ChapterA.conjCLM_unitScale` (α : V ≃ₗᵢ[ℂ] W) (l : ℂ) (hl : ‖l‖ = 1) (m : V →L[ℂ] V) : conjCLM (α.trans (unitScaleEquiv l hl)) m = conjCLM α m

Initializing...

`BookProof.ChapterA.conjCLM_unitScale` (α : V ≃ₗᵢ[ℂ] W) (l : ℂ) (hl : ‖l‖ = 1) (m : V →L[ℂ] V) : conjCLM (α.trans (unitScaleEquiv l hl)) m = conjCLM α m · Prove2Me