Skip to content

Commit

Permalink
chore: bump SHA in Data/ENat/Basic (#3178)
Browse files Browse the repository at this point in the history
* [`data.enat.basic`@`9003f28797c0664a49e4179487267c494477d853`..`ceb887ddf3344dab425292e497fa2af91498437c`](https://leanprover-community.github.io/mathlib-port-status/file/data/enat/basic?range=9003f28797c0664a49e4179487267c494477d853..ceb887ddf3344dab425292e497fa2af91498437c)

The change in mathlib3 is irrelevant, as `coe_zero` is no longer a simp lemma.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed Mar 30, 2023
1 parent 915c292 commit 55a5c6b
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/ENat/Basic.lean
Expand Up @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
! This file was ported from Lean 3 source module data.enat.basic
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! leanprover-community/mathlib commit ceb887ddf3344dab425292e497fa2af91498437c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down

0 comments on commit 55a5c6b

Please sign in to comment.