Skip to content

Commit

Permalink
fix(equiv/ring): fix bad typeclasses on ring_equiv.trans_apply (#7258)
Browse files Browse the repository at this point in the history
`ring_equiv.trans` had weaker typeclasses than the lemma which unfolds it.
  • Loading branch information
eric-wieser committed Apr 19, 2021
1 parent 77f5fb3 commit 184e0fe
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/data/equiv/ring.lean
Expand Up @@ -158,9 +158,8 @@ symm_bijective.injective $ ext $ λ x, rfl
@[trans] protected def trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : R ≃+* S' :=
{ .. (e₁.to_mul_equiv.trans e₂.to_mul_equiv), .. (e₁.to_add_equiv.trans e₂.to_add_equiv) }

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

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

0 comments on commit 184e0fe

Please sign in to comment.