Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Feb 25, 2024

• feat: small_iUnion and small_sUnion (leanprover-community#10921)

  TwoFX

  committedFeb 25, 2024
  89415b3

• fix: typo (leanprover-community#10966)

  kbuzzard

  committedFeb 25, 2024
  dc217ae

• chore: bump dependencies (leanprover-community#10954)

  

  semorrison

  and

  riccardobrasca

  committedFeb 25, 2024
  a62da66

• fix(Algebra/DirectSum/Ring): correct mis-ported lemma names (leanprover-community#10953)

  

  eric-wieser

  and

  timotree3

  committedFeb 25, 2024
  a3692d9

• chore: fix port of join_filter_isEmpty_eq_false (leanprover-community#10951)

  

  semorrison

  and

  eric-wieser

  committedFeb 25, 2024
  23adc28

• feat: Subsingleton.pairwise (leanprover-community#10938)

  jsm28

  committedFeb 25, 2024
  68312f0

• chore: classify removed @[nolint has_nonempty_instance] porting notes (leanprover-community#10929)

  pitmonticone

  committedFeb 25, 2024
  2599c3b

• chore: bump aesop; update syntax (leanprover-community#10955)

  semorrison

  committedFeb 25, 2024
  46974e9

• chore: split Ordered instances for subobjects into separate files (leanprover-community#10900)

  

  mattrobball

  and

  eric-wieser

  committedFeb 25, 2024
  46be277

• chore: omit a proof in CategoryTheory/Limits/Cones that aesop now does (leanprover-community#10947)

  semorrison

  committedFeb 25, 2024
  46beab5

• chore(Measure.MeasureSpace): clean up uses of @ (leanprover-community#10932)

  

  mattrobball

  and

  kbuzzard

  committedFeb 25, 2024
  4cf5bbb

• feat: breadcrumb path for assert_not_exists (leanprover-community#10940)

  

  digama0

  and

  semorrison

  committedFeb 25, 2024
  3505618

• refactor(UniformConvergenceTopology): redefine using UniformOnFun (leanprover-community#10873)

  urkud

  committedFeb 25, 2024
  a36350f

Commits on Feb 24, 2024

• chore(NormedSpace/Basic): rename type variables (leanprover-community#10863)

  urkud

  committedFeb 24, 2024
  c8eaa18

• chore(diamonds): appropriate transparency levels for diamond checks (leanprover-community#10910)

  

  mattrobball

  and

  kbuzzard

  committedFeb 24, 2024
  29c854d

• feat(CategoryTheory/Monoidal/Mon_): add simp lemmas (leanprover-community#10905)

  yuma-mizuno

  committedFeb 24, 2024
  13ae635

• feat: full subcategory for a small set is essentially small (leanprover-community#10922)

  TwoFX

  committedFeb 24, 2024
  4dd3701

• chore: classify added lemma porting notes (leanprover-community#10926)

  pitmonticone

  committedFeb 24, 2024
  6af752e

• chore: classify added instance porting notes (leanprover-community#10925)

  pitmonticone

  committedFeb 24, 2024
  1d96f99

• feat: Add Module.End.baseChangeHom (leanprover-community#10928)

  eric-wieser

  committedFeb 24, 2024
  fd1b047

• fix(RingTheory/RootsOfUnity/Basic): generalise some results to monoids (leanprover-community#10605)

  kbuzzard

  committedFeb 24, 2024
  cf96395

• chore(MeasureTheory): move Measure/OuterMeasure to OuterMeasure/Basic (leanprover-community#10916)

  urkud

  committedFeb 24, 2024
  d3dbfd9

• chore(StdBasis): Fintype -> Finite (leanprover-community#10914)

  urkud

  committedFeb 24, 2024
  a25ebf0

• feat(GroupTheory/Perm/ClosureSwap): A transitive permutation group generated by transpositions must be the whole symmetric group (leanprover-community#10035)

  tb65536

  committedFeb 24, 2024
  d6542aa

• feat: final functors with filtered codomain (leanprover-community#10892)

  TwoFX

  committedFeb 24, 2024
  558a4f9

• chore(CategoryTheory/Limits): Fintype -> Finite (leanprover-community#10915)

  urkud

  committedFeb 24, 2024
  1caa43c

• chore: rename arguments to PiTensorProduct induction principles (leanprover-community#10904)

  eric-wieser

  committedFeb 24, 2024
  5ac4fc9

• feat(RingTheory): hopf algebra definition (leanprover-community#10079)

  

  3 peoplecommittedFeb 24, 2024
  ee8d1db

• chore(CategoryTheory): remove an unnecessary instance and golf a proof in the effective epi file (leanprover-community#10734)

  dagurtomas

  committedFeb 24, 2024
  9a891c3

Commits on Feb 23, 2024

• chore(CategoryTheory/Sites): golf and tidy up proof that extensive+regular generate coherent (leanprover-community#10903)

  dagurtomas

  committedFeb 23, 2024
  3c38b01

• feat(FieldTheory/Adjoin): add IntermediateField.[fin]rank_bot' (leanprover-community#10896)

  acmepjz

  committedFeb 23, 2024
  c951d81

• feat(Algebra/Associated): add Associated.map (leanprover-community#10895)

  acmepjz

  committedFeb 23, 2024
  0fb7df8

• feat: push forward FinallySmall along a final functor (leanprover-community#10894)

  TwoFX

  committedFeb 23, 2024
  64d2ea8

• feat: final functors with filtered domain (leanprover-community#10720)

  TwoFX

  committedFeb 23, 2024
  10079c6

• feat(LinearAlgebra/Matrix): define projective special linear group (leanprover-community#7791)

  

  3 peoplecommittedFeb 23, 2024
  fec1a64

Pagination

PreviousNext