chore(algebra): clean up some imports

Also add some notation to lean-input.el

hott/algebra/bundled.hlean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad
 
 Bundled structures
 -/
-import algebra.group homotopy.interval
+import algebra.group
 open algebra pointed is_trunc
 
 namespace algebra

hott/algebra/field.hlean

@@ -6,7 +6,7 @@ Authors: Robert Lewis
 Structures with multiplicative and additive components, including division rings and fields.
 The development is modeled after Isabelle's library.
 -/
-import algebra.binary algebra.group algebra.ring
+import algebra.ring
 open eq eq.ops algebra
 set_option class.force_new true
 

hott/algebra/homomorphism.hlean

@@ -5,7 +5,7 @@ Author: Jeremy Avigad
 
 Homomorphisms between structures.
 -/
-import algebra.ring algebra.category.category
+import algebra.ring function
 open eq function is_trunc
 
 namespace algebra

hott/algebra/order.hlean

@@ -5,7 +5,7 @@ Author: Jeremy Avigad
 
 Weak orders "≤", strict orders "<", and structures that include both.
 -/
-import algebra.binary algebra.priority
+import algebra.binary
 open eq eq.ops algebra
 -- set_option class.force_new true
 

hott/algebra/ordered_group.hlean

@@ -6,7 +6,7 @@ Authors: Jeremy Avigad
 Partially ordered additive groups, modeled on Isabelle's library. These classes can be refined
 if necessary.
 -/
-import algebra.binary algebra.group algebra.order
+import algebra.group algebra.order
 open eq eq.ops algebra   -- note: ⁻¹ will be overloaded
 set_option class.force_new true
 

hott/algebra/ring.hlean

@@ -7,7 +7,7 @@ Structures with multiplicative and additive components, including semirings, rin
 The development is modeled after Isabelle's library.
 -/
 
-import algebra.binary algebra.group
+import algebra.group
 open eq eq.ops algebra
 set_option class.force_new true
 

hott/homotopy/EM.hlean

@@ -465,8 +465,6 @@ namespace EM
     { exact EMadd1_functor φ n }
   end
 
-  -- TODO: (K G n →* K H n) ≃ (G →g H)
-
   /- Equivalence of Groups and pointed connected 1-truncated types -/
 
   definition ptruncconntype10_pequiv (X Y : 1-Type*[0]) (e : π₁ X ≃g π₁ Y) : X ≃* Y :=

src/emacs/lean-input.el

@@ -357,6 +357,8 @@ order for the change to take effect."
   ("-1v"       . ("⁻¹ᵛ"))
   ("-1E"       . ("⁻¹ᴱ"))
   ("-1hty"     . ("⁻¹ʰᵗʸ"))
+  ("-1lm"      . ("⁻¹ˡᵐ"))
+  ("-1gm"      . ("⁻¹ᵍᵐ"))
   ("-2"        . ("⁻²" "₋₂"))
   ("-2o"       . ("⁻²ᵒ"))
   ("-3"        . ("⁻³"))