chore(algebra/tropical/basic): golf and clean (#10633)

leanprover-community · Dec 8, 2021 · fdb773a · fdb773a
1 parent bcd9a74
commit fdb773a
Showing 1 changed file with 25 additions and 17 deletions.
diff --git a/src/algebra/tropical/basic.lean b/src/algebra/tropical/basic.lean
@@ -263,33 +263,41 @@ instance [add_comm_semigroup R] : comm_semigroup (tropical R) :=
 { mul_comm := λ _ _, untrop_injective (add_comm _ _),
   ..tropical.semigroup }
 
-instance [add_monoid R] : monoid (tropical R) :=
-{ one := trop 0,
-  one_mul := λ _, untrop_injective (zero_add _),
-  mul_one := λ _, untrop_injective (add_zero _),
-  npow := λ n x, trop (n • untrop x),
-  npow_zero' := trop_rec (λ _, by simp only [trop_zero, zero_smul]),
-  npow_succ' := λ _, trop_rec (λ _, by simp only [succ_nsmul, untrop_trop, trop_add]),
-  ..tropical.semigroup }
+instance {α : Type*} [has_scalar α R] : has_pow (tropical R) α :=
+{ pow := λ x n, trop $ n • untrop x }
 
-@[simp] lemma untrop_pow [add_monoid R] (x : tropical R) (n : ℕ) :
+@[simp] lemma untrop_pow {α : Type*} [has_scalar α R] (x : tropical R) (n : α) :
   untrop (x ^ n) = n • untrop x := rfl
 
+@[simp] lemma trop_smul {α : Type*} [has_scalar α R] (x : R) (n : α) :
+  trop (n • x) = trop x ^ n := rfl
+
+instance [add_zero_class R] : mul_one_class (tropical R) :=
+{ one := 1,
+  mul := (*),
+  one_mul := λ _, untrop_injective $ zero_add _,
+  mul_one := λ _, untrop_injective $ add_zero _ }
+
+instance [add_monoid R] : monoid (tropical R) :=
+{ npow := λ n x, x ^ n,
+  npow_zero' := λ _, untrop_injective $ zero_smul _ _,
+  npow_succ' := λ _ _, untrop_injective $ succ_nsmul _ _,
+  ..tropical.mul_one_class,
+  ..tropical.semigroup }
+
 @[simp] lemma trop_nsmul [add_monoid R] (x : R) (n : ℕ) :
   trop (n • x) = trop x ^ n := rfl
 
 instance [add_comm_monoid R] : comm_monoid (tropical R) :=
 { ..tropical.monoid, ..tropical.comm_semigroup }
 
 instance [add_group R] : group (tropical R) :=
-{ inv := λ x, trop (- untrop x),
-  mul_left_inv := λ _, untrop_injective (add_left_neg _),
-  zpow := λ n x, trop (n • untrop x),
-  zpow_zero' := trop_rec (λ _, by simp only [zero_zsmul, trop_zero]),
-  zpow_succ' := λ _, trop_rec (λ _, untrop_injective
-    (by simp only [succ_nsmul, of_nat_zsmul, untrop_trop, trop_add])),
-  zpow_neg' := λ _, trop_rec (λ _, untrop_injective
-    (by simp only [zsmul_neg_succ_of_nat, untrop_trop, untrop_pow, coe_nat_zsmul])),
+{ inv := has_inv.inv,
+  mul_left_inv := λ _, untrop_injective $ add_left_neg _,
+  zpow := λ n x, trop $ n • untrop x,
+  zpow_zero' := λ _, untrop_injective $ zero_zsmul _,
+  zpow_succ' := λ _ _, untrop_injective $ add_group.zsmul_succ' _ _,
+  zpow_neg' := λ _ _, untrop_injective $ add_group.zsmul_neg' _ _,
   ..tropical.monoid }
 
 instance [add_comm_group R] : comm_group (tropical R) :=