Theorems · Theorem · complex analysis

RCLike.sqrt_map

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {𝕜' : Type u_2} [inst_1 : RCLike 𝕜'] {a : 𝕜},
  RCLike.im RCLike.I = RCLike.im RCLike.I → RCLike.sqrt ((RCLike.map 𝕜 𝕜') a) = (RCLike.map 𝕜 𝕜') (RCLike.sqrt a)

Defined in

Mathlib.Analysis.RCLike.Sqrt

Cited by

0 results in Mathlib

Foundations

Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeRCLike