Commit 2025-02-13 07:36 e7b0826e

View on Github →

chore(WithBot): rename unbot' to unbotD (#21532)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean

added theorem WithBot.unbotD_one

deleted theorem WithBot.unbot_one'

added theorem WithTop.untopD_one

deleted theorem WithTop.untop_one'

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

deleted theorem WithBot.unbot'_zero_mul

added theorem WithBot.unbotD_zero_mul

deleted theorem WithTop.untop'_zero_mul

added theorem WithTop.untopD_zero_mul

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Modified Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finite.lean

Modified Mathlib/Data/ENNReal/Basic.lean

Modified Mathlib/Data/ENNReal/Real.lean

Modified Mathlib/Data/ENat/Basic.lean

modified def ENat.toNat

modified theorem ENat.toNat_eq_zero

Modified Mathlib/Data/List/MinMax.lean

deleted theorem List.getD_max?_eq_unbot'_maximum

added theorem List.getD_max?_eq_unbotD_maximum

deleted theorem List.getD_min?_eq_untop'_minimum

added theorem List.getD_min?_eq_untopD_minimum

Modified Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

Modified Mathlib/Order/GaloisConnection/Basic.lean

deleted def WithBot.giUnbot'Bot

added def WithBot.giUnbotDBot

Modified Mathlib/Order/KrullDimension.lean

Modified Mathlib/Order/WithBot.lean

deleted theorem WithBot.le_coe_unbot'

added theorem WithBot.le_coe_unbotD

deleted def WithBot.unbot'

deleted theorem WithBot.unbot'_bot

deleted theorem WithBot.unbot'_coe

deleted theorem WithBot.unbot'_eq_iff

deleted theorem WithBot.unbot'_eq_self_iff

deleted theorem WithBot.unbot'_eq_unbot'_iff

deleted theorem WithBot.unbot'_le_iff

deleted theorem WithBot.unbot'_lt_iff

added def WithBot.unbotD

added theorem WithBot.unbotD_bot

added theorem WithBot.unbotD_coe

added theorem WithBot.unbotD_eq_iff

added theorem WithBot.unbotD_eq_self_iff

added theorem WithBot.unbotD_eq_unbotD_iff

added theorem WithBot.unbotD_le_iff

added theorem WithBot.unbotD_lt_iff

deleted theorem WithTop.coe_untop'_le

added theorem WithTop.coe_untopD_le

deleted theorem WithTop.le_untop'_iff

added theorem WithTop.le_untopD_iff

deleted theorem WithTop.lt_untop'_iff

added theorem WithTop.lt_untopD_iff

deleted def WithTop.untop'

deleted theorem WithTop.untop'_coe

deleted theorem WithTop.untop'_eq_iff

deleted theorem WithTop.untop'_eq_self_iff

deleted theorem WithTop.untop'_eq_untop'_iff

deleted theorem WithTop.untop'_top

added def WithTop.untopD

added theorem WithTop.untopD_coe

added theorem WithTop.untopD_eq_iff

added theorem WithTop.untopD_eq_self_iff

added theorem WithTop.untopD_eq_untopD_iff

added theorem WithTop.untopD_top

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/Tactic/ComputeDegree.lean