mathlib

2511faf4 - feat(tactic/localized): localized notation (#1081)

feat(tactic/localized): localized notation (#1081) * first prototype of localized notation * update * add test file * shorten command, fix test * update documentation * rename files, add to tactic/default * typo * mention that we can use other commands * optimize * only use 1 attribute * add localized command classical instance * use rb_lmap This changes the internal code to avoid import clashes and adds a test to that effect * move rb_lmap.of_list to correct file also update docstring * rename open_notation to open_locale