Commits

Branch selector

 master

User selector

All users

Datepicker

All time

Commit History

Commits on Dec 16, 2024

• feat(SetTheory/Game/PGame): identical_of_eq (#19983)

  Show description for 3f813de
  tristan-f-r

  committed
  3f813de

  Copy full SHA for 3f813de

• chore(Algebra/Group/Nat): Remove some unnecessary lemmas arguments (#19981)

  IvanRenison

  committed
  d3319ca

  Copy full SHA for d3319ca

• feat(SetTheory/Ordinal/Arithmetic): `(sInf sᶜ).card ≤ #s` (#18780)

  Show description for dd3f45b
  vihdzp

  committed
  dd3f45b

  Copy full SHA for dd3f45b

• feat(SetTheory/Cardinal/Arithmetic): cardinality of ordinal exponential (#17813)

  Show description for 9e10768
  vihdzp

  committed
  9e10768

  Copy full SHA for 9e10768

Commits on Dec 15, 2024

• chore(SetTheory/Ordinal/NaturalOps): address porting notes (#19237)

  Show description for 00a4da3
  vihdzp

  committed
  00a4da3

  Copy full SHA for 00a4da3

• chore: revert removal of tactic usage in Archive (#19974)

  Show description for ffcd1a0
  kim-em

  committed
  ffcd1a0

  Copy full SHA for ffcd1a0

• chore: rename Mathlib.Vector to List.Vector (#19930)

  Show description for 07a5460
  kim-em

  committed
  07a5460

  Copy full SHA for 07a5460

• feat: add theorems about isLUB and isGLB for Finset.sup and Finset.inf (#19961)

  Show description for af60d5d
  pauldavidrowe

  committed
  af60d5d

  Copy full SHA for af60d5d

• feat(SetTheory/ZFC/Basic): generalize universes of `range` (#17016)

  vihdzp

  committed
  7ce82ed

  Copy full SHA for 7ce82ed

• feat(SetTheory/ZFC/Ordinal): Alternate characterizations of ordinals (#17001)

  Show description for 161b962
  vihdzp

  committed
  161b962

  Copy full SHA for 161b962

• chore(scripts): update nolints.json (#19971)

  Show description for a395cd0
  leanprover-community-bot

  committed
  a395cd0

  Copy full SHA for a395cd0

• feat(SetTheory/ZFC/Basic): `x ∈ y → ¬ y ⊆ x` (#19967)

  vihdzp

  committed
  86f77db

  Copy full SHA for 86f77db

• chore(SetTheory/ZFC/Rank): clean up file (#18239)

  Show description for ecf9698
  vihdzp

  committed
  ecf9698

  Copy full SHA for ecf9698

Commits on Dec 14, 2024

• feat(Algebra/Category/Grp/ForgetCorepresentable, Algebra/Category/MonCat/ForgetCorepresentable): the forgetful functor on the category of monoids is corepresentable (#19964)

  Show description for 37a149f
  

  smorel394

  committed
  37a149f

  Copy full SHA for 37a149f

• doc(Algebra/Category/Ring/Basic): fix copy-paste errors (#19962)

  eric-wieser

  committed
  8fe8834

  Copy full SHA for 8fe8834

• refactor(GroupTheory/SpecificGroups/Cyclic): Extract `MulEquiv` from `IsCyclic.card_mulAut` (#19948)

  Show description for 1ed7634
  tb65536

  committed
  1ed7634

  Copy full SHA for 1ed7634

• feat: volume of Euclidean balls in even and odd dimensions (#19949)

  Show description for 197eebf
  j-loreaux

  committed
  197eebf

  Copy full SHA for 197eebf

• chore: make some `induction_on*` compatible with `induction` (#19898)

  urkud

  committed
  e2b3244

  Copy full SHA for e2b3244

• feat(SetTheory/Cardinal/Cofinality): generalize `cof_preOmega` (#19916)

  Show description for b8d0621
  vihdzp

  committed
  b8d0621

  Copy full SHA for b8d0621

• chore(discover-lean-pr-testing): only consider branches with "lean-pr-testing" in the name (#19958)

  Show description for 79d29f8
  

  jcommelin

  and

  adomani

  committed
  79d29f8

  Copy full SHA for 79d29f8

• feat: drop an assumption in `mfderivWithin_const` (#19936)

  Show description for 468b507
  sgouezel

  committed
  468b507

  Copy full SHA for 468b507

• style(Algebra/Category/Grp/Basic and Algebra/Category/MonCat/Basic): universe order in `uliftFunctor` (#19957)

  Show description for b09464f
  

  smorel394

  committed
  b09464f

  Copy full SHA for b09464f

• feat(CategoryTheory/Monoidal): composition of monoidal category adjunctions (#17956)

  Show description for d19d840
  joelriou

  committed
  d19d840

  Copy full SHA for d19d840

• perf: replace many instances of 'linarith' with 'omega' (#19951)

  Show description for ce0a54c
  dwrensha

  committed
  ce0a54c

  Copy full SHA for ce0a54c

• feat: more lemmas about the cocompact filter on topological spaces with a continuous multiplication and zero (#19650)

  Show description for 0662d0b
  trivial1711

  committed
  0662d0b

  Copy full SHA for 0662d0b

Commits on Dec 13, 2024

• feat(FieldTheory/Finite/Basic): `(1 + p * a) ^ (p ^ m) ≡ 1 [MOD p ^ m]` (#19881)

  Show description for d1fa45b
  tb65536

  committed
  d1fa45b

  Copy full SHA for d1fa45b

• feat(NumberTheory/Padics/RingHoms): add the equivalence between the residue field of Z_p and ZMod p (#19922)

  Show description for 73ea8d5
  faenuccio

  committed
  73ea8d5

  Copy full SHA for 73ea8d5

• feat(Topology/Algebra/Group/Basic): a quotient map between topological groups is open (#19657)

  Show description for 76cecbb
  kbuzzard

  committed
  76cecbb

  Copy full SHA for 76cecbb

• feat(CategoryTheory/Enriched): Add eHomCongr and related lemmas (#19932)

  Show description for 5aaaf8b
  gio256

  committed
  5aaaf8b

  Copy full SHA for 5aaaf8b

• fix: ensure the clashing `X[i]` notations have the same precedence (#19900)

  Show description for b0a22ed
  eric-wieser

  committed
  b0a22ed

  Copy full SHA for b0a22ed

• feat(Algebra/Category): categories of modules have the same AB axioms as abelian groups (#19939)

  dagurtomas

  committed
  98dbd12

  Copy full SHA for 98dbd12

• refactor(Algebra/Category/Ring): make morphisms a structure (#19757)

  Show description for ddbd495
  

  chrisflav

  and

  Vierkantor

  committed
  ddbd495

  Copy full SHA for ddbd495

• chore: move `Polynomial.basisMonomials` to a separate file (#19933)

  Show description for 658f649
  acmepjz

  committed
  658f649

  Copy full SHA for 658f649

• chore: shorten proof of le_iff_sub_nonneg (#19925)

  tomaz1502

  committed
  2f5c967

  Copy full SHA for 2f5c967

• feat(Combinatorics/SimpleGraph): Add theorem `two_le_chromaticNumber_of_adj` (#19924)

  IvanRenison

  committed
  0310194

  Copy full SHA for 0310194

Pagination

Previous

Next