mathlib3

ca80c8b0 - feat(data/nat/sqrt_norm_num): norm_num extension for sqrt (#12735)

feat(data/nat/sqrt_norm_num): norm_num extension for sqrt (#12735) Inspired by https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/2.20is.20not.20a.20square . The norm_num extension has to go in a separate file from `data.nat.sqrt` because `data.nat.sqrt` is a dependency of `norm_num`.