isConformalMap_iff

theorem isConformalMap_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] (f : E →L[ℝ] F), IsConformalMap f ↔ ∃ c, 0 < c ∧ ∀ (u v : E), ⟪f u, f v⟫_ℝ = c * ⟪u, v⟫_ℝ

The theorem `isConformalMap_iff` states that for any continuous linear map `f` between two inner product spaces `E` and `F`, the map is conformal if and only if it preserves inner products up to a scalar factor. More specifically, there exists a positive real number `c` such that the inner product of the images of any two vectors `u` and `v` under `f` is equal to `c` times the inner product of `u` and `v`. In mathematical form, this is `⟪f u, f v⟫ = c * ⟪u, v⟫` for all vectors `u`, `v` in the inner product space `E`.

More concisely: A continuous linear map between two inner product spaces is conformal if and only if it preserves inner products up to a positive scalar factor. Equivalently, there exists a positive real number `c` such that `⟪f u, f v⟫ = c * ⟪u, v⟫` for all vectors `u` and `v` in the inner product space.