Why does it say "unknown constant 'Real.Sqrt'"?

Stream: mathlib4

[Lewis]

def l2_norm {n : ℕ} (v : Vec n) : ℝ :=

  Real.Sqrt (∑ i, (v i) ^ 2)

Why does it say "unknown constant 'Real.Sqrt'"? Thanks.

[Riccardo Brasca]

You have to import the file defining it. Starting with

import Mathlib

will import everything.

[Lewis]

Riccardo Brasca said:

You have to import the file defining it. Starting with

import Mathlib

will import everything.

I did that:

import Mathlib.Data.Real.Basic

import Mathlib.Algebra.Module.Basic

import Mathlib.Data.Fin.Basic

import Mathlib.Data.Matrix.Basic

import Mathlib.Topology.Basic
--import Mathlib.data.real.basic

open Real

open Matrix

Why does it still say "unknown constant 'Real.Sqrt'"? Thanks.

[Floris van Doorn]

Searching for docs#Real.sqrt will teach you that the definition is in Mathlib.Data.Real.Sqrt, you have to import that.

For your next issue, take a look at #backticks and #mwe.

[Floris van Doorn]

You will also be interested to know about docs#EuclideanSpace, which defined the type \R^n with the usual norm/inner product.

[Yaël Dillies]

Mostly, isn't the function called Real.sqrt, not Real.Sqrt?

[Kyle Miller]

Something I do to search for the right name is move my cursor to the end of Real.Sqrt and do ctrl+space (or whatever your autocomplete keybinding is) to get a list of some possibilities. It works only if what you have is a subset of the correct letters.

image.png