leanprover-community/mathlib

Pull Requests Commits
the additive group as an abelian group scheme
joelriou committed 3 years ago
c56f57a3
preadditive structure
joelriou committed 3 years ago
a362d8ca
some progress
joelriou committed 3 years ago
f443d4b8
equivalence from Ab to internal Ab Type
joelriou committed 3 years ago
8ee5acd9
starting showing that internal Ab Type is equivalent to Ab
joelriou committed 3 years ago
8c3be63f
little progress
joelriou committed 3 years ago
240bdb14
some progress
joelriou committed 3 years ago
1159d956
some progress
joelriou committed 3 years ago
75adbfbb
definition of modules
joelriou committed 3 years ago
a2e48d8b
tidying the code
joelriou committed 3 years ago
630e1fbc
little progress
joelriou committed 3 years ago
facdf187
some progress
joelriou committed 3 years ago
208c0503
Ring
joelriou committed 3 years ago
33bbaa51
smul
joelriou committed 3 years ago
8868121c
some progress
joelriou committed 3 years ago
90650e90
some progress
joelriou committed 3 years ago
282b6b9e
some progress
joelriou committed 3 years ago
dc2d467d
some progress
joelriou committed 3 years ago
479a66ba
some progress
joelriou committed 3 years ago
83eb6c23
draft
joelriou committed 3 years ago
9484a655
feat(scripts/port_status): script to show currently portable files (#17009)
kim-em committed 3 years ago
6d4f6107
feat(*): add various order-related lemmas (#16918)
ocfnash committed 3 years ago
a5347cb9
feat(analysis/calculus/cont_diff): strengthen lemma (#16933)
fpvandoorn committed 3 years ago
38992f94
feat(combinatorics/simple_graph/regularity/bound): `positivity` extension (#16639)
YaelDillies committed 3 years ago
8f774b71
feat(data/polynomial): a couple of lemmas on nat degree and roots of maps (#16992)
alexjbest committed 3 years ago
d8dd620c
feat(ring_theory/finiteness): A morphism is finitely presented if the composition with a finite morphism is. (#15949)
erdOne committed 3 years ago
cf94743b
feat(topology/subset_properties, noetherian_space): Noetherian spaces have finite irreducible components. (#17015)
erdOne committed 3 years ago
6d94ff7b
refactor(geometry/manifold/cont_mdiff): split everything about mfderiv (#16982)
fpvandoorn committed 3 years ago
2b69cd5e
style(geometry/euclidean): consistently use inner product notation (#16961)
jsm28 committed 3 years ago
3c95a727
feat(algebraic_geometry/prime_spectrum/basic): intersection of localisations (#16860)
Multramate committed 3 years ago
5f17f4da
Terms Of Use Privacy Policy Refund Policy Impressum