Commit 2023-07-19 08:39 d3b4f0c8

View on Github →

chore: bump quote4 (#5975)

Estimated changes

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/Tactic/ModCases.lean

Modified Mathlib/Tactic/NormNum/Basic.lean

modified def Mathlib.Meta.NormNum.evalEq

modified def Mathlib.Meta.NormNum.evalLE

modified def Mathlib.Meta.NormNum.evalLT

modified def Mathlib.Meta.NormNum.evalMkRat

modified def Mathlib.Meta.NormNum.evalNatSucc

Modified Mathlib/Tactic/NormNum/BigOperators.lean

Modified Mathlib/Tactic/NormNum/GCD.lean

Modified Mathlib/Tactic/NormNum/IsCoprime.lean

Modified Mathlib/Tactic/NormNum/LegendreSymbol.lean

modified def Tactic.NormNum.evalJacobiSym

modified def Tactic.NormNum.evalJacobiSymNat

modified def Tactic.NormNum.evalLegendreSym

Modified Mathlib/Tactic/NormNum/Prime.lean

Modified Mathlib/Tactic/Positivity/Core.lean

Modified Mathlib/Tactic/Ring/Basic.lean

Modified Mathlib/Util/Qq.lean

deleted theorem Qq.QE.rfl

added theorem Qq.QuotedDefEq.rfl

Modified lake-manifest.json