jcommelin

-- Written by Johan Commelin; golfed by Kenny Lau

import tactic.interactive

universe u

namespace eckmann_hilton
variables (X : Type u)

local notation a `<`m`>` b := @has_mul.mul X m a b