Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 1ac8d43

Browse files
committed
chore(*): fix @[to_additive, simp] to the correct order (#19169)
Whilst making some files, I noticed that there is some lemmas that have the wrong order for `to_additive` and `simp`.
1 parent c321606 commit 1ac8d43

File tree

3 files changed

+5
-5
lines changed

3 files changed

+5
-5
lines changed

src/algebra/hom/equiv/basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -309,10 +309,10 @@ fun_like.ext _ _ e.apply_symm_apply
309309
theorem self_trans_symm (e : M ≃* N) : e.trans e.symm = refl M :=
310310
fun_like.ext _ _ e.symm_apply_apply
311311

312-
@[to_additive, simp] lemma coe_monoid_hom_refl {M} [mul_one_class M] :
312+
@[simp, to_additive] lemma coe_monoid_hom_refl {M} [mul_one_class M] :
313313
(refl M : M →* M) = monoid_hom.id M := rfl
314314

315-
@[to_additive, simp] lemma coe_monoid_hom_trans {M N P}
315+
@[simp, to_additive] lemma coe_monoid_hom_trans {M N P}
316316
[mul_one_class M] [mul_one_class N] [mul_one_class P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
317317
(e₁.trans e₂ : M →* P) = (e₂ : N →* P).comp ↑e₁ :=
318318
rfl

src/group_theory/subsemigroup/center.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -151,7 +151,7 @@ end
151151
section
152152
variables (M) [comm_semigroup M]
153153

154-
@[to_additive, simp] lemma center_eq_top : center M = ⊤ :=
154+
@[simp, to_additive] lemma center_eq_top : center M = ⊤ :=
155155
set_like.coe_injective (set.center_eq_univ M)
156156

157157
end

src/topology/algebra/monoid.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -698,14 +698,14 @@ variables [has_mul X] [has_continuous_mul X]
698698
@[to_additive "The continuous map `λ y, y + x"]
699699
protected def mul_right (x : X) : C(X, X) := mk _ (continuous_mul_right x)
700700

701-
@[to_additive, simp]
701+
@[simp, to_additive]
702702
lemma coe_mul_right (x : X) : ⇑(continuous_map.mul_right x) = λ y, y * x := rfl
703703

704704
/-- The continuous map `λ y, x * y` -/
705705
@[to_additive "The continuous map `λ y, x + y"]
706706
protected def mul_left (x : X) : C(X, X) := mk _ (continuous_mul_left x)
707707

708-
@[to_additive, simp]
708+
@[simp, to_additive]
709709
lemma coe_mul_left (x : X) : ⇑(continuous_map.mul_left x) = λ y, x * y := rfl
710710

711711
end continuous_map

0 commit comments

Comments
 (0)