Commit 2024-08-29 01:14 331465fa

View on Github →

chore(Order): move some defs to a new file (#16202)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/ENat/Basic.lean

deleted def ENat.recTopCoe

deleted theorem ENat.recTopCoe_coe

deleted theorem ENat.recTopCoe_top

deleted def ENat

Modified Mathlib/Data/PNat/Defs.lean

deleted def PNat.val

deleted def PNat

Modified Mathlib/Data/Set/Image.lean

Modified Mathlib/Order/Interval/Set/WithBotTop.lean

Modified Mathlib/Order/Notation.lean

Created Mathlib/Order/TypeTags.lean

added def ENat.recTopCoe

added theorem ENat.recTopCoe_coe

added theorem ENat.recTopCoe_top

added def ENat

added def PNat.val

added def PNat

added def WithBot.recBotCoe

added theorem WithBot.recBotCoe_bot

added theorem WithBot.recBotCoe_coe

added def WithBot.some

added def WithBot

added def WithTop.recTopCoe

added theorem WithTop.recTopCoe_coe

added theorem WithTop.recTopCoe_top

added def WithTop.some

added def WithTop

Modified Mathlib/Order/WithBot.lean

deleted def WithBot.recBotCoe

deleted theorem WithBot.recBotCoe_bot

deleted theorem WithBot.recBotCoe_coe

deleted def WithBot.some

deleted def WithBot

deleted def WithTop.recTopCoe

deleted theorem WithTop.recTopCoe_coe

deleted theorem WithTop.recTopCoe_top

deleted def WithTop.some

deleted def WithTop

Modified test/lift.lean