Changelog

feat(Data/Finite/Card): `Nat.card`/`ENat.card` is strictly monotonic on finite sets (#34693)

chore: remove `Ideal.span_singleton_le_iff_mem` as explicit simp argument (#35498) …

ci: Secure proofwidgets fetches on cache get (#35463) …

chore(CategoryTheory/Limits): dualize (parts of) `pullback.diagonal` (#35454) …

chore(Data/Set/Defs): move `ext` attribute to `Set.ext` (#35485)

chore: update Mathlib dependencies 2026-02-18 (#35506) …

fix: disable backward.isDefEq.respectTransparency globally (#35500) …

feat(Analysis/Normed/Operator/Compact): criteria for compactness of the identity operator (#35196) …

fix(Dynamics/BirkhoffSum): birkhoffAverage_of_comp_eq only needs AddCommMonoid (#35307)

chore: remove redundant `Aesop` imports (#35474) …

feat: neighborhood basis in a metric space consisting of closed balls of radius `1 / (n + 1)` (#35207)

doc: `PFun.fix_induction` to `PFun.fixInduction` (#35199) …

feat: generalize some results for `SupConvergenceClass` to `ConditionallyCompletePartialOrder{Sup,Inf}` (#35050)

chore: clean up `sSup` and `sInf` usage (#35297)

style(RingTheory/PowerSeries/Derivative): prove derivative_pow from Derivation.leibniz_pow (#35067)

chore(Tactic): improve `contrapose` tactic documentation (#35492) …

feat(Ideal/Span): add Ideal.span_singleton_le_iff_mem to simp set (#35489)

feat: define `LinearMap.piMap` and `ContinuousLinearMap.piMap` (#35430) …

feat: the normal closure of an empty set is the trivial subgroup (#35029) …

chore(RamificationInertia): remove an unnecessary hypothesis in `inertiaDeg_algebraMap` (#35483)

chore: modulize tests (2/N) (#35288)

feat(Topology/Algebra/Star/LinearMap): intrinsic star for continuous linear maps (#33397)

chore: simplify statement of `Module.End.isNilpotent_isSemisimple_unique` (#35471)

feat(Geometry/Convex/Cone): monotonicity and map lemmas for min/max cone tensor products (#34383) …

feat(Topology): Connecting different notions of locally finite (#26259) …

feat(NumberTheory/Height/Projectivization): new file (#34780) …

feat(Algebra/Polynomial/Lifts): Add `mem_lifts_and_support_eq` (#35132) …

chore: fix inexistent `NE.ne` namespace (#35466) …

refactor(Analysis/Calculus): redefine `HasFDerivAtFilter` (#34965) …

chore: update Mathlib dependencies 2026-02-18 (#35468) …

ci: Enable telemetry pump for nightly-testing runs (#35462) …

chore: bump toolchain to v4.29.0-rc1 (#35459)

chore(MeasureTheory): fix indentation in markdown lists (#35443) …

chore(CategoryTheory/Limits): add instances for `HasPullback f.op g.op` and `HasPushout f.op g.op` (#35453) …

feat(Data/Set/PowersetCard): definitions on `Set.powersetCard` (#35432) …

feat(Topology/Connected/PathConnected): relate `ZerothHomotopy` and `ConnectedComponents` (#34244)

ci: Use variable instead of secret for OTLP_ENDPOINT (#35457) …

feat(AlgebraicGeometry): infinitesimal lifting criterion for formally unramified morphisms (#35397)

feat(Analysis/InnerProductSpace/Basic): variants of the parallelogram law with squaring (#35171) …

chore(RingTheory/RingHom/Locally): rename `locally_StableUnderComposition…` to `locally_stableUnderComposition…` (#35147) …

chore(MetricSpace/Antilipschitz): the antilipschitz constant is positive for nontrivial metric spaces (#35227) …

ci: Add documentation/status page for workflows (#35112) …

feat(Topology/ContinuousMap/LocallyConstant): the range of `toContinuousMapAlgHom` separates points (#35221) …

chore: update Mathlib dependencies 2026-02-17 (#35449) …

feat: binomial random graphs (#31364) …

feat(InformationTheory/Coding): Kraft-McMillan inequality for uniquely decodable codes (#34108) …

refactor(Computability): file for state transition systems (#33291) …

feat(Topology/Algebra/Group/Basic): group is totally disconnected iff `connectedComponent 1 = {1}` (#35404) …

ci: add `splice-bot` action (#33979) …

chore: fix printf error in nightly bump Zulip message (#35428) …