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

Commit 184e0fe

Browse files
committed
fix(equiv/ring): fix bad typeclasses on ring_equiv.trans_apply (#7258)
`ring_equiv.trans` had weaker typeclasses than the lemma which unfolds it.
1 parent 77f5fb3 commit 184e0fe

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

src/data/equiv/ring.lean

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -158,9 +158,8 @@ symm_bijective.injective $ ext $ λ x, rfl
158158
@[trans] protected def trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : R ≃+* S' :=
159159
{ .. (e₁.to_mul_equiv.trans e₂.to_mul_equiv), .. (e₁.to_add_equiv.trans e₂.to_add_equiv) }
160160

161-
@[simp] lemma trans_apply {A B C : Type*}
162-
[semiring A] [semiring B] [semiring C] (e : A ≃+* B) (f : B ≃+* C) (a : A) :
163-
e.trans f a = f (e a) := rfl
161+
@[simp] lemma trans_apply (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) :
162+
e₁.trans e₂ a = e₂ (e₁ a) := rfl
164163

165164
protected lemma bijective (e : R ≃+* S) : function.bijective e := e.to_equiv.bijective
166165
protected lemma injective (e : R ≃+* S) : function.injective e := e.to_equiv.injective

0 commit comments

Comments
 (0)