# Documentation

Mathlib.Tactic.ScopedNS

# scoped[NS] syntax #

This is a replacement for the localized command in mathlib. It is similar to scoped, but it scopes the syntax in the specified namespace instead of the current namespace.

scoped[NS] is similar to the scoped modifier on attributes and notations, but it scopes the syntax in the specified namespace instead of the current namespace.

scoped[Matrix] infixl:75 " ⬝ " => Matrix.mul
-- declares ⬝ as a notation for matrix multiplication
-- which is only accessible if you open Matrix or open scoped Matrix.

namespace Nat

scoped[Nat.Count] attribute [instance] CountSet.fintype
-- make the definition Nat.CountSet.fintype an instance,
-- but only if Nat.Count is open
⬝ " => Matrix.mul
-- declares ⬝ as a notation for matrix multiplication
-- which is only accessible if you open Matrix or open scoped Matrix.

namespace Nat

scoped[Nat.Count] attribute [instance] CountSet.fintype
-- make the definition Nat.CountSet.fintype an instance,
-- but only if Nat.Count is open
⬝ as a notation for matrix multiplication
-- which is only accessible if you open Matrix or open scoped Matrix.

namespace Nat

scoped[Nat.Count] attribute [instance] CountSet.fintype
-- make the definition Nat.CountSet.fintype an instance,
-- but only if Nat.Count is open
`
Equations
• One or more equations did not get rendered due to their size.