imperialcollegelondon/flt issues and pull requests

#97 - Completed a few sorries in HIMExperiments/module_topology.lean

Pull Request - State: closed - Opened by scholzhannah 5 months ago

#96 - Bump mathlib

Pull Request - State: closed - Opened by Ruben-VandeVelde 5 months ago - 1 comment

#95 - Update blueprint for exists_near

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#94 - Patch 1

Pull Request - State: closed - Opened by ahhwuhu 6 months ago - 1 comment

#93 - Fix LaTeX error and warning

Pull Request - State: closed - Opened by pitmonticone 6 months ago

#92 - Prove Hurwitz.exists_near

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#91 - fix blueprint

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#90 - left_ideal_princ

Pull Request - State: closed - Opened by FLDutchmann 6 months ago - 1 comment

#89 - Bump mathlib

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#88 - Injections into QHat

Pull Request - State: closed - Opened by Timeroot 6 months ago - 1 comment

#87 - 'and now everything follows' for quot_rem

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 4 comments

#86 - Bump rexml from 3.2.5 to 3.2.8 in /docs

Pull Request - State: closed - Opened by dependabot[bot] 6 months ago - 1 comment

#85 - Bump nokogiri from 1.13.6 to 1.16.5 in /docs

Pull Request - State: closed - Opened by dependabot[bot] 6 months ago - 1 comment

#84 - Crazy affine

Pull Request - State: closed - Opened by Whysoserioushah 6 months ago - 1 comment

#83 - Update blueprint

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#82 - Bump mathlib

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#81 - Add missing `leanok` to lemma 6.2

Pull Request - State: closed - Opened by Rida-Hamadani 6 months ago - 2 comments

#80 - Norm

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#79 - Star

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#78 - Add missing `leanok` to lemma 5.13

Pull Request - State: closed - Opened by Rida-Hamadani 6 months ago - 1 comment

#77 - A matrix ring is a central simple algebra

Pull Request - State: closed - Opened by trivial1711 6 months ago - 2 comments

#76 - Ring instance for Hurwitz

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#75 - Add Hurwitz.toQuaternion

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#74 - Multiplication for Hurwitz numbers

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#73 - lowestTerms

Pull Request - State: open - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#72 - e_not_in_Int

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#71 - typo

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#70 - Update the blueprint for #51.

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#69 - a not-ready proof

Issue - State: open - Opened by kbuzzard 6 months ago

#68 - Fix `hyperref` warning

Pull Request - State: closed - Opened by pitmonticone 6 months ago - 1 comment

#67 - every tensor in QHat is pure

Pull Request - State: closed - Opened by dagurtomas 6 months ago - 1 comment

#66 - ZHat is torsion-free

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#65 - reconnect the blueprint

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#64 - finish ZHat.multiples

Pull Request - State: closed - Opened by dagurtomas 6 months ago - 1 comment

#63 - Fix minor typos

Pull Request - State: closed - Opened by DavidMichaelRoberts 6 months ago - 1 comment

#62 - Fix typos in docstrings

Pull Request - State: closed - Opened by pitmonticone 6 months ago - 1 comment

#61 - CharZero ZHat

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago

#60 - e ∈ ZHat

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#59 - Fix typos in chapter 5 and 6

Pull Request - State: closed - Opened by pitmonticone 6 months ago - 1 comment

#58 - Adjust namespaces for `Coalgebra`, and remove a heartbeat bump

Pull Request - State: closed - Opened by eric-wieser 6 months ago - 1 comment

#57 - Update to the newer lakefile format

Pull Request - State: closed - Opened by eric-wieser 6 months ago - 3 comments

#56 - fix statement of ZHat.multiples

Pull Request - State: closed - Opened by dagurtomas 6 months ago - 1 comment

#55 - ZHat is a ring

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 1 comment

#54 - chore: bump lean to v4.8.0-rc1

Pull Request - State: closed - Opened by Ruben-VandeVelde 6 months ago - 2 comments

#53 - Mention etale cohomology

Issue - State: open - Opened by kbuzzard 6 months ago

#52 - TODO: make FLT.lean more interesting

Issue - State: closed - Opened by kbuzzard 6 months ago - 2 comments

#51 - feat: simplify proof of ¬FreyPackage -> FLT

Pull Request - State: closed - Opened by digama0 6 months ago - 1 comment

#50 - half of MatrixRing.isCentralSimple

Pull Request - State: closed - Opened by Ruben-VandeVelde 7 months ago - 1 comment

#49 - Test

Pull Request - State: closed - Opened by riccardobrasca 7 months ago

#48 - typos

Pull Request - State: closed - Opened by Ruben-VandeVelde 7 months ago - 1 comment

#47 - MatrixRing.isCentralSimple

Issue - State: closed - Opened by kbuzzard 7 months ago - 1 comment

#46 - update blueprint

Pull Request - State: closed - Opened by Ruben-VandeVelde 7 months ago

#45 - Fix macOS (?) issue with latin modern math font

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 3 comments

#44 - Substitute `\cite` to `\ref` in `chtopbestiary.tex`

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 3 comments

#43 - Add missing $ in `ch03frey.tex`

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 1 comment

#42 - Fix typo in `Reductions.lean`

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 1 comment

#41 - Remove `.venv` from `.gitignore`

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 1 comment

#40 - Homogenise and tidy .bib file

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 3 comments

#39 - wip: FreyCurve.j_valuation_of_bad_prime

Pull Request - State: closed - Opened by Ruben-VandeVelde 7 months ago - 1 comment

#38 - feat: FreyCurve.j

Pull Request - State: closed - Opened by Ruben-VandeVelde 7 months ago - 1 comment

#37 - Package `fontspec` Error: font "Latin Modern Math" cannot be found

Issue - State: closed - Opened by pitmonticone 7 months ago - 1 comment

#36 - Fix \cite and local pdf compilation

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 2 comments

#35 - Fix label bug

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 1 comment

#34 - Update .gitignore

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 1 comment

#33 - typo: arithemtic

Pull Request - State: closed - Opened by Ruben-VandeVelde 7 months ago - 1 comment

#32 - define "locally free" and state that it is equivalent to "flat" for finitely presented modules

Pull Request - State: closed - Opened by trivial1711 7 months ago - 4 comments

#31 - Fix typos in the blueprint

Pull Request - State: closed - Opened by peabrainiac 7 months ago - 1 comment

#30 - feat: define the Frey curve

Pull Request - State: closed - Opened by trivial1711 7 months ago - 1 comment

#29 - feat: fill in of_not_FermatLastTheorem_coprime_p_ge_5

Pull Request - State: closed - Opened by Ruben-VandeVelde 7 months ago - 3 comments

#28 - feat: discriminant of P.FreyCurve

Pull Request - State: closed - Opened by Ruben-VandeVelde 7 months ago - 1 comment

#27 - fix typo, add to .gitignore

Pull Request - State: closed - Opened by digama0 7 months ago - 4 comments

#26 - Theorems -> Theorem

Pull Request - State: closed - Opened by Julian 7 months ago - 1 comment

#25 - Add comment about FLT3 and fix other typos

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 1 comment

#24 - Fix typos in blueprint, docstrings and notes

Pull Request - State: closed - Opened by pitmonticone 7 months ago - 1 comment

#23 - Compatible families of Galois representations

Issue - State: open - Opened by kbuzzard 7 months ago - 1 comment

#22 - Test new CI

Pull Request - State: closed - Opened by PatrickMassot 7 months ago

#21 - FLT.FreyCurve

Issue - State: closed - Opened by kbuzzard 7 months ago

#20 - Fix blueprint workflow

Pull Request - State: closed - Opened by PatrickMassot 7 months ago - 1 comment

#19 - `FLT.FreyPackage.of_not_FermatLastTheorem`

Issue - State: closed - Opened by kbuzzard 7 months ago - 2 comments

#18 - Add Frobenius elements

Pull Request - State: closed - Opened by jouglasheen 8 months ago - 7 comments

#17 - Update lakefile.lean for checkdecls

Pull Request - State: closed - Opened by PatrickMassot 8 months ago

#16 - `fermatLastTheoremThree`

Issue - State: closed - Opened by kbuzzard 8 months ago

#15 - feat: tidy up co/bi/hopf algebra

Pull Request - State: closed - Opened by jjaassoonn 8 months ago - 1 comment

#14 - Yunzhou xie hopf

Pull Request - State: closed - Opened by Whysoserioushah 8 months ago - 1 comment

#13 - HopfAlgebra

Pull Request - State: closed - Opened by Whysoserioushah 8 months ago - 1 comment

#12 - Formalising Mathematics projects

Issue - State: closed - Opened by kbuzzard 9 months ago - 1 comment

#11 - showmore is fixed in leanblueprint

Pull Request - State: closed - Opened by utensil 11 months ago - 1 comment

#10 - Fix CI

Pull Request - State: closed - Opened by utensil 11 months ago - 1 comment

#9 - Fix PDF bookmark string in section title

Pull Request - State: closed - Opened by utensil 11 months ago

#8 - Build both PDF and web in texlive-action

Pull Request - State: closed - Opened by utensil 12 months ago

#7 - Build both PDF and web in texlive-action (failed)

Pull Request - State: closed - Opened by utensil 12 months ago

#6 - Fix Mathlib search after caching

Pull Request - State: closed - Opened by utensil 12 months ago

#5 - Try accelerating LaTeX building

Pull Request - State: closed - Opened by utensil 12 months ago - 1 comment

#4 - Add Gitpod for more instant access and collaboration

Pull Request - State: closed - Opened by utensil 12 months ago

#3 - Misc fixes to the blueprint per requested

Pull Request - State: closed - Opened by utensil 12 months ago

#2 - Add `inv dev` for local testing

Pull Request - State: closed - Opened by utensil 12 months ago

#1 - Initial setup of the blueprint, docs and the project page

Pull Request - State: closed - Opened by utensil 12 months ago

GitHub / imperialcollegelondon/flt issues and pull requests