Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Mar 16, 2025

• feat: induction principles for strongly measurable functions (#22960)

  Show description for 76e119d
  EtienneC30

  committed
  76e119d

  Copy full SHA for 76e119d

• feat(CategoryTheory): Noetherian objects (#22373)

  Show description for 3ef10a6
  joelriou

  committed
  3ef10a6

  Copy full SHA for 3ef10a6

• chore: move List.Lex lemmas out of the List.Lex namespace (#22935)

  Show description for bce45b1
  YaelDillies

  committed
  bce45b1

  Copy full SHA for bce45b1

• feat(Data/Complex/Trigonometric): closer upper bound for cos 1 (#22945)

  Show description for 36a0240
  vlad902

  committed
  36a0240

  Copy full SHA for 36a0240

• feat: API for continuous extension of meromorphic functions (#22867)

  Show description for 3a94488
  kebekus

  committed
  3a94488

  Copy full SHA for 3a94488

• feat(LinearAlgebra/FreeModule/CardQuotient): compute indices of subgroups via determinant (#22940)

  xroblot

  committed
  f988aab

  Copy full SHA for f988aab

• perf(CategoryTheory/Limits/Shapes): reorder instance arguments (#22968)

  Show description for 48ecbcb
  JovanGerb

  committed
  48ecbcb

  Copy full SHA for 48ecbcb

Commits on Mar 15, 2025

• feat: add norm_num extensions for factorials (#8832)

  Show description for e4e8796
  

  sebzim4500

  and

  eric-wieser

  committed
  e4e8796

  Copy full SHA for e4e8796

• chore(Ideal/Quotient): change Fintype to Finite (#22947)

  Show description for 14bdbbd
  xroblot

  committed
  14bdbbd

  Copy full SHA for 14bdbbd

• docs(Data/Real/EReal): fix capitalization error (#22943)

  Show description for edd97d2
  plp127

  committed
  edd97d2

  Copy full SHA for edd97d2

• feat(FieldTheory/Finite/Basic): lemmas about the prime subfield in positive characteristic (#22843)

  Show description for 4104be5
  ScottCarnahan

  committed
  4104be5

  Copy full SHA for 4104be5

• chore(Order/Group/Abs): use @[to_additive] (#22468)

  urkud

  committed
  e390e20

  Copy full SHA for e390e20

• feat: scalar tower instances for quotients (#22951)

  Show description for a6a5c8d
  eric-wieser

  committed
  a6a5c8d

  Copy full SHA for a6a5c8d

• doc: fix typo (#22946)

  EtienneC30

  committed
  ec9bcd0

  Copy full SHA for ec9bcd0

• chore: drop Algebra.Order.Ring.Nat import from Data.Nat.Count (#22941)

  Ruben-VandeVelde

  committed
  1c3b40c

  Copy full SHA for 1c3b40c

• feat(Combinatorics/SimpleGraph): define Copy (#20658)

  Show description for 3543cd8
  mitchell-horner

  committed
  3543cd8

  Copy full SHA for 3543cd8

• feat: move Nat.count_le_cardinal, add variants (#22938)

  Ruben-VandeVelde

  committed
  bae5286

  Copy full SHA for bae5286

Commits on Mar 14, 2025

• doc: add library note about the continuous functional calculus (#22172)

  j-loreaux

  committed
  5ad1c5b

  Copy full SHA for 5ad1c5b

• chore: unsimp Set.prod_singleton (#22937)

  YaelDillies

  committed
  56bfc1e

  Copy full SHA for 56bfc1e

• refactor(Algebra/Group/Subgroup/Basic): clean up normalizer lemmas (#22913)

  Show description for f47e8d6
  tb65536

  committed
  f47e8d6

  Copy full SHA for f47e8d6

• feat: more lemmas on NatOrdinal (#22616)

  Show description for be8a170
  vihdzp

  committed
  be8a170

  Copy full SHA for be8a170

• feat(ContinuousMonoidHom): add notation for ContinuousMonoidHom and ContinuousAddMonoidHom (#21300)

  Show description for c529790
  rmhi

  committed
  c529790

  Copy full SHA for c529790

• refactor(AlgebraicTopology/SimplicialSet): use the Subpresheaf API (#21090)

  Show description for cc79638
  joelriou

  committed
  cc79638

  Copy full SHA for cc79638

• chore: tidy various files (#22894)

  Ruben-VandeVelde

  committed
  3afb029

  Copy full SHA for 3afb029

• feat: for nilpotent derivations, exponential is multiplicative (#22875)

  Show description for 8b48c43
  ocfnash

  committed
  8b48c43

  Copy full SHA for 8b48c43

• refactor(FreeModule/IdealQuotient): Generalize to submodule of full rank (#22902)

  Show description for 17b56b4
  xroblot

  committed
  17b56b4

  Copy full SHA for 17b56b4

• feat(Topology/UniformSpace): define nonarchimedean uniformity (#22580)

  Show description for 4a709c3
  

  pechersky

  and

  leanprover-community-mathlib4-bot

  committed
  4a709c3

  Copy full SHA for 4a709c3

• chore: rename induction_on''' (#22848)

  Show description for 561c554
  BoltonBailey

  committed
  561c554

  Copy full SHA for 561c554

• feat: preimage of a product by restrict (#22558)

  Show description for f59312e
  EtienneC30

  committed
  f59312e

  Copy full SHA for f59312e

• chore(CategoryTheory): remove local truncated simplicial notation (#22906)

  Show description for 0e29a68
  emilyriehl

  committed
  0e29a68

  Copy full SHA for 0e29a68

• chore: review of erw in Topology/ (#22914)

  kim-em

  committed
  65468c4

  Copy full SHA for 65468c4

• chore(Data): go through remaining porting notes (#22907)

  Show description for f033aca
  Vierkantor

  committed
  f033aca

  Copy full SHA for f033aca

• feat: Galois groups of finite fields (#22885)

  alreadydone

  committed
  d633863

  Copy full SHA for d633863

• chore(Analysis/Normed/Lp/WithLp): generalize action-related instances on WithLp (#22706)

  Show description for b6dd454
  qawbecrdtey

  committed
  b6dd454

  Copy full SHA for b6dd454

Commits on Mar 13, 2025

• chore(Algebra/Group/Basic): rename mul_right_eq_self to mul_eq_left etc (#22587)

  Show description for c9d2c01
  b-reinke

  committed
  c9d2c01

  Copy full SHA for c9d2c01

Pagination

Previous

Next