Commit 2026-10-27 21:33 afcc9cd1

View on Github →

chore: use IsApply for CauSeq (#45101) I had to fix some defeq abuse in CauSeq along the way.

Estimated changes

Modified Mathlib/Algebra/Order/CauSeq/Basic.lean

deleted theorem CauSeq.add_apply

modified theorem CauSeq.ext

added def CauSeq.mk

added theorem CauSeq.mk_apply

deleted theorem CauSeq.mul_apply

deleted theorem CauSeq.neg_apply

deleted theorem CauSeq.one_apply

deleted theorem CauSeq.pow_apply

deleted theorem CauSeq.smul_apply

deleted theorem CauSeq.sub_apply

deleted theorem CauSeq.zero_apply

Modified Mathlib/Algebra/Order/CauSeq/Completion.lean

Modified Mathlib/Analysis/Complex/Exponential.lean

Modified Mathlib/Analysis/Complex/Norm.lean

added theorem Complex.cauSeqConj_apply

added theorem Complex.cauSeqIm_apply

added theorem Complex.cauSeqNorm_apply

added theorem Complex.cauSeqRe_apply

Modified Mathlib/Analysis/Fourier/PoissonSummation.lean

Modified Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean

Modified Mathlib/NumberTheory/Padics/PadicNumbers.lean

Modified Mathlib/NumberTheory/Padics/RingHoms.lean

Modified Mathlib/Topology/MetricSpace/CauSeqFilter.lean

Modified MathlibTest/InstanceDiamonds.lean