Request for explanation about the syntax ![x,y]

Stream: lean4

[aprilgrimoire]

Hi! In mathlib code, I saw the following syntax:

/-- Also see `LinearIndependent.pair_iff'` for a simpler version over fields. -/
lemma LinearIndependent.pair_iff {x y : M} :
    LinearIndependent R ![x, y] ↔ ∀ (s t : R), s • x + t • y = 0 → s = 0 ∧ t = 0 := by
  refine ⟨fun h s t hst ↦ h.eq_zero_of_pair hst, fun h ↦ ?_⟩
  apply Fintype.linearIndependent_iff.2
  intro g hg
  simp only [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons] at hg
  intro i
  fin_cases i
  exacts [(h _ _ hg).1, (h _ _ hg).2]

I wonder what does ![x, y] mean? I don't remember seeing any explanations for it in the tutorials.

[Ruben Van de Velde]

It's notation for the function Fin 2 → M that sends zero to x and one to y`

[aprilgrimoire]

Ruben Van de Velde said:

It's notation for the function Fin 2 → M that sends zero to x and one to y`

Thanks. Where can I find documentation for such things, or are there even any clickable things regarding such syntax?

[Ruben Van de Velde]

If I put my cursor between ! and [ and hit F12 in vs code, it takes me to https://github.com/leanprover-community/mathlib4/blob/4969d8c2185478d362c5b9eb8fd8684a3c80ee7c/Mathlib/Data/Fin/VecNotation.lean#L68

[Patrick Massot]

It is explained in https://leanprover-community.github.io/mathematics_in_lean/C09_Linear_Algebra.html#matrices-bases-and-dimension

[Eric Wieser]

I think the "adding vectors" line is wrong there