Skip to content

Commit

Permalink
chore(*): fix @[to_additive, simp] to the correct order (#19169)
Browse files Browse the repository at this point in the history
Whilst making some files, I noticed that there is some lemmas that have the wrong order for `to_additive` and `simp`.
  • Loading branch information
ericrbg committed Jun 14, 2023
1 parent c321606 commit 1ac8d43
Show file tree
Hide file tree
Showing 3 changed files with 5 additions and 5 deletions.
4 changes: 2 additions & 2 deletions src/algebra/hom/equiv/basic.lean
Expand Up @@ -309,10 +309,10 @@ fun_like.ext _ _ e.apply_symm_apply
theorem self_trans_symm (e : M ≃* N) : e.trans e.symm = refl M :=
fun_like.ext _ _ e.symm_apply_apply

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

@[to_additive, simp] lemma coe_monoid_hom_trans {M N P}
@[simp, to_additive] lemma coe_monoid_hom_trans {M N P}
[mul_one_class M] [mul_one_class N] [mul_one_class P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
(e₁.trans e₂ : M →* P) = (e₂ : N →* P).comp ↑e₁ :=
rfl
Expand Down
2 changes: 1 addition & 1 deletion src/group_theory/subsemigroup/center.lean
Expand Up @@ -151,7 +151,7 @@ end
section
variables (M) [comm_semigroup M]

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

end
Expand Down
4 changes: 2 additions & 2 deletions src/topology/algebra/monoid.lean
Expand Up @@ -698,14 +698,14 @@ variables [has_mul X] [has_continuous_mul X]
@[to_additive "The continuous map `λ y, y + x"]
protected def mul_right (x : X) : C(X, X) := mk _ (continuous_mul_right x)

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

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

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

end continuous_map

0 comments on commit 1ac8d43

Please sign in to comment.