Commit 2024-06-10 07:27 38962a38

View on Github →

chore(*): drop some bit0/bit1 lemmas (#13679) Since bit0 and bit1 are deprecated in Lean 4, these lemmas were deprecated for a long time. Also move Filter.nonneg_of_eventually_pow_nonneg to Order/Filter/ModEq.

Estimated changes

Modified Mathlib/Algebra/Algebra/Hom.lean

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

deleted theorem WithBot.coe_bit0

deleted theorem WithBot.coe_bit1

deleted theorem WithTop.coe_bit0

deleted theorem WithTop.coe_bit1

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

deleted theorem Polynomial.aeval_bit0

deleted theorem Polynomial.aeval_bit1

Modified Mathlib/Algebra/Polynomial/Derivative.lean

deleted theorem Polynomial.derivative_bit0

deleted theorem Polynomial.derivative_bit1

Modified Mathlib/Algebra/Polynomial/Eval.lean

Modified Mathlib/Algebra/Ring/Basic.lean

deleted theorem map_bit0

Modified Mathlib/Algebra/Ring/Hom/Defs.lean

deleted theorem map_bit1

Modified Mathlib/Algebra/Star/Basic.lean

deleted theorem star_bit0

deleted theorem star_bit1

Modified Mathlib/Algebra/Star/Module.lean

Modified Mathlib/Algebra/Star/SelfAdjoint.lean

deleted theorem IsSelfAdjoint.bit0

deleted theorem IsSelfAdjoint.bit1

deleted theorem skewAdjoint.bit0_mem

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

deleted theorem Zsqrtd.bit0_im

deleted theorem Zsqrtd.bit0_re

deleted theorem Zsqrtd.bit1_im

deleted theorem Zsqrtd.bit1_re

Modified Mathlib/Order/Filter/AtTopBot.lean

deleted theorem Filter.nonneg_of_eventually_pow_nonneg

deleted theorem Filter.tendsto_bit0_atBot

deleted theorem Filter.tendsto_bit0_atTop

deleted theorem Filter.tendsto_bit1_atTop

Modified Mathlib/Order/Filter/ModEq.lean

added theorem Filter.nonneg_of_eventually_pow_nonneg