Skip to content

Commit

Permalink
Browse files Browse the repository at this point in the history
This change was already applied in a previous forward-port in order to fix compilation. The porting note can now be removed, since mathlib3 now contains the same generalization.

* [`algebra.star.self_adjoint`@`9abfa6f0727d5adc99067e325e15d1a9de17fd8e`..`a6ece35404f60597c651689c1b46ead86de5ac1b`](https://leanprover-community.github.io/mathlib-port-status/file/algebra/star/self_adjoint?range=9abfa6f0727d5adc99067e325e15d1a9de17fd8e..a6ece35404f60597c651689c1b46ead86de5ac1b)
  • Loading branch information
eric-wieser committed Apr 2, 2023
1 parent 8945882 commit fcca249
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions Mathlib/Algebra/Star/SelfAdjoint.lean
Expand Up @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Frédéric Dupuis
! This file was ported from Lean 3 source module algebra.star.self_adjoint
! leanprover-community/mathlib commit 9abfa6f0727d5adc99067e325e15d1a9de17fd8e
! leanprover-community/mathlib commit a6ece35404f60597c651689c1b46ead86de5ac1b
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -252,7 +252,6 @@ end DivisionRing

section Semifield

-- porting note: generalize to `Semifield` to fix lean4#2074-related errors
variable [Semifield R] [StarRing R]

theorem div {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x / y) := by
Expand Down

0 comments on commit fcca249

Please sign in to comment.