Commits

Branch selector

 master

User selector

ocfnash

Datepicker

All time

Commit History

Commits on Nov 17, 2025

• feat: miscellaneous root system lemmas (#29147)

  ocfnash

  committed
  e6a0ede

  Copy full SHA for e6a0ede

Commits on Nov 10, 2025

• chore: state `writtenInExtChartAt_comp` using `Filter.EventuallyEq` (#31469)

  ocfnash

  committed
  3f2ecb3

  Copy full SHA for 3f2ecb3

Commits on Oct 24, 2025

• feat: if the order topology for a dense linear ordering is discrete, the space has at most one point (#30856)

  Show description for 39cfbec
  

  ocfnash

  and

  Aristotle-Harmonic

  committed
  39cfbec

  Copy full SHA for 39cfbec

Commits on Oct 9, 2025

• chore: drastically speed up `LieModule.Cohomology.d₂₃` (#30377)

  Show description for 6955cd0
  

  ocfnash

  and

  Vierkantor

  committed
  6955cd0

  Copy full SHA for 6955cd0

Commits on Sep 15, 2025

• feat: equivalence of `Complex.IsConservativeOn` and `DifferentiableOn ℂ` for continuous functions on open sets (#29629)

  ocfnash

  committed
  df4ef40

  Copy full SHA for df4ef40

Commits on Sep 1, 2025

• feat: a root system is determined by its Cartan matrix (#29052)

  Show description for 035d719
  ocfnash

  committed
  035d719

  Copy full SHA for 035d719

Commits on Aug 20, 2025

• feat: the Geck construction yields (finite-dimensional) semisimple Lie algebras (#27237)

  Show description for 9bac717
  ocfnash

  committed
  9bac717

  Copy full SHA for 9bac717

Commits on Aug 19, 2025

• chore: fix defeq abuse in `WithVal` (#28597)

  Show description for a79ea2e
  ocfnash

  committed
  a79ea2e

  Copy full SHA for a79ea2e

Commits on Aug 11, 2025

• chore: split file `LinearAlgebra.RootSystem.GeckConstruction.Basic` (#28089)

  Show description for 337e0bc
  ocfnash

  committed
  337e0bc

  Copy full SHA for 337e0bc

• feat: roots of a root system are determined by their pairings with elements of a base (#28086)

  Show description for eac80b1
  ocfnash

  committed
  eac80b1

  Copy full SHA for eac80b1

• feat: drop assumption `[P.IsNotG2]` in lemma `RootPairing.lie_e_f_ne` (#28011)

  Show description for 16d91fe
  ocfnash

  committed
  16d91fe

  Copy full SHA for 16d91fe

• feat: the Geck Construction yields trace-free matrices (#27831)

  Show description for 9439afe
  ocfnash

  committed
  9439afe

  Copy full SHA for 9439afe

Commits on Aug 6, 2025

• feat: miscellaneous Lie algebra lemmas (#27600)

  Show description for c3f0f19
  ocfnash

  committed
  c3f0f19

  Copy full SHA for c3f0f19

Commits on Aug 5, 2025

• feat: basic linear algebra lemmas about matrices (#27605)

  Show description for e074407
  ocfnash

  committed
  e074407

  Copy full SHA for e074407

Commits on Aug 4, 2025

• feat: add naming hint to doc string of `LinearMap.proj` (#27685)

  Show description for d59ab0f
  ocfnash

  committed
  d59ab0f

  Copy full SHA for d59ab0f

Commits on Aug 3, 2025

• feat: a finite union of proper submodules is a proper subset (#27598)

  Show description for ad1449f
  ocfnash

  committed
  ad1449f

  Copy full SHA for ad1449f

Commits on Jul 17, 2025

• feat: add root system induction principle equivalent to connectedness of Dynkin diagram (#26965)

  Show description for 5e820da
  ocfnash

  committed
  5e820da

  Copy full SHA for 5e820da

Commits on Jul 8, 2025

• feat: add induction principle for positive roots relative to a base of a root system (#26819)

  ocfnash

  committed
  1aa6f29

  Copy full SHA for 1aa6f29

• feat: add lemma 3.5 from [Geck](https://dx.doi.org/10.1090/proc/13600) (#26592)

  Show description for 350e70c
  ocfnash

  committed
  350e70c

  Copy full SHA for 350e70c

Commits on Jul 7, 2025

• chore: reorganise root system files associated with Geck construction (#26849)

  Show description for 58ff372
  ocfnash

  committed
  58ff372

  Copy full SHA for 58ff372

• chore: use typeclass rather than implicit arguments for decidability data (#26662)

  Show description for 5e4c8bc
  ocfnash

  committed
  5e4c8bc

  Copy full SHA for 5e4c8bc

Commits on Jun 18, 2025

• feat: add simp to lemma `Fin.coe_ofNat_eq_mod` (#26095)

  Show description for 6ef9cd8
  ocfnash

  committed
  6ef9cd8

  Copy full SHA for 6ef9cd8

Commits on Jun 7, 2025

• feat: an invertible matrix as a perfect pairing (#25477)

  Show description for 6f872f1
  ocfnash

  committed
  6f872f1

  Copy full SHA for 6f872f1

Commits on Jun 5, 2025

• feat: One-point compactification of Euclidean space homeomorphic to sphere (#18711)

  Show description for a6e2960
  

  ocfnash

  and

  bjoernkjoshanssen

  committed
  a6e2960

  Copy full SHA for a6e2960

Commits on Jun 4, 2025

• chore: add `deprecated_module`s for renamed one-point compactification files (#25399)

  ocfnash

  committed
  05f31f4

  Copy full SHA for 05f31f4

• chore: reorganise files about one-point compactification (#25426)

  Show description for 0af34fc
  ocfnash

  committed
  0af34fc

  Copy full SHA for 0af34fc

Commits on Jun 2, 2025

• feat: implement Geck's construction of a Lie algebra associated to a root system with distinguished base (#25285)

  ocfnash

  committed
  ce1e4be

  Copy full SHA for ce1e4be

• feat: various lemmas to support construction of Lie algebra from root system (#25214)

  ocfnash

  committed
  0298271

  Copy full SHA for 0298271

Commits on May 19, 2025

• feat: define the `sl₂` Lie subalgebra associated to a root (#24995)

  Show description for 9c5f0d6
  ocfnash

  committed
  9c5f0d6

  Copy full SHA for 9c5f0d6

• feat: add characterisation of irreducible root pairing using `IsSimpleOrder` (#24958)

  ocfnash

  committed
  396cbfc

  Copy full SHA for 396cbfc

Commits on May 7, 2025

• feat: Cartan matrices are non-singular (#24639)

  Show description for 8e49c5f
  ocfnash

  committed
  8e49c5f

  Copy full SHA for 8e49c5f

Commits on May 6, 2025

• feat: add Geck's final root system lemma for implementing Lusztig construction (#24263)

  Show description for 0da9417
  

  ocfnash

  and

  jcommelin

  committed
  0da9417

  Copy full SHA for 0da9417

Commits on May 2, 2025

• chore: highlight locations which may provide examples for speeding up `aesop` (#24552)

  Show description for 1031377
  ocfnash

  committed
  1031377

  Copy full SHA for 1031377

Commits on May 1, 2025

• feat: add supporting API for Geck's final root system lemma (#24476)

  Show description for 820df42
  ocfnash

  committed
  820df42

  Copy full SHA for 820df42

Commits on Apr 17, 2025

• feat: add lemma `Submodule.length_lt` (#24133)

  Show description for 1f4ab9d
  ocfnash

  committed
  1f4ab9d

  Copy full SHA for 1f4ab9d

Pagination

Previous

Next