leanprover-community/mathlib

Pull Requests Commits

feat(set_theory/ordinal/basic): add `gc_ord_card` and `gci_ord_card` (#15152)

urkud committed 3 years ago

b36a458a

feat(data/multiset/fintype): coercion from multiset to type (#15094)

kmill committed 3 years ago

b9c17c14

refactor(set_theory/game/pgame): tweak `relabelling` definition (#14941)

vihdzp committed 3 years ago

00c39680

feat(set_theory/game/ordinal): lemmas on `0.to_pgame` and `1.to_pgame` (#14780)

vihdzp committed 3 years ago

b90e72c7

feat(topology/homotopy): define nth homotopy group πₙ (without the group instance) (#14724)

ralvrz committed 3 years ago

3600b621

feat(combinatorics/simple_graph/subgraph): delete vertices in a subgraph (#14403)

kmill committed 3 years ago

e960dc61

feat(algebra/module): add injective module and Baer's criterion (#12895)

jjaassoonn committed 3 years ago

fcaedc52

feat(data/{finset,set}/basic): `insert a s = s ↔ a ∈ s` (#15493)

YaelDillies committed 3 years ago

5a017443

chore(data/json): add a missing subtype parser for nullable types (#15486)

eric-wieser committed 3 years ago

9540a420

feat(topology/basic): add 2 lemmas about `locally_finite` families (#15485)

urkud committed 3 years ago

3557e4dc

feat(data/list/infix): drop_while and take_while suf/prefix (#15473)

pechersky committed 3 years ago

a26b4ee8

chore(algebra/group/ulift): add missing lemmas about pow, additivize (#15469)

eric-wieser committed 3 years ago

925d8909

fix(analysis/locally_convex): weaken assumptions for `totally_bounded.is_vonN_bounded` (#15468)

ADedecker committed 3 years ago

8d2ae95f

doc(set_theory/ordinal/cantor_normal_form): implementation notes (#15466)

vihdzp committed 3 years ago

2cdc7579

refactor(tactic/polyrith): use the autogenerated json parser (#15429)

eric-wieser committed 3 years ago

92f31fbc

feat(set_theory/cardinal/ordinal): cardinality of `α →₀ β` (#15198)

vihdzp committed 3 years ago

0b673ed4

feat(data/vector/mem): Lemmas about membership in a vector (#15154)

dtumad committed 3 years ago

f5d916a6

feat(data/nat/choose/basic): Definition of `multichoose` and basic lemmas (#15072)

stuart-presnell committed 3 years ago

4af7cb21

feat(ring_theory/bezout): Bezout domains are integrally closed (#15424)

erdOne committed 3 years ago

7b43177d

refactor(order/compactly_generated): Generalize `submodule.exists_finset_of_mem_supr` to compact elements of complete lattices (#15419)

tb65536 committed 3 years ago

ee72cf62

feat(ring_theory/localization/basic): section of localisation of non-zero is non-zero (#15404)

Multramate committed 3 years ago

0e30f2da

feat(algebraic_geometry/EllipticCurve): simplify definition of discriminant (#15365)

digama0 committed 3 years ago

582e6672

refactor(data/finset/lattice): sup' and inf' without option (#15195)

pechersky committed 3 years ago

bcc2c4e4

feat(tactic/congrm): add "function underscores" to `congrm` (#14532)

adomani committed 3 years ago

9c7a7cca

feat(algebra/module/localized_module): construction of module localisation (#14470)

jjaassoonn committed 3 years ago

fba86201

feat(ring_theory/adjoin_root): add lemmas for GCD domains (#14981)

riccardobrasca committed 3 years ago

903e8941

feat(data/real/{e,}nnreal): images and preimages of `ord_connected` sets (#15483)

urkud committed 3 years ago

b60a2703

feat(data/list/basic): last_reverse (#15482)

pechersky committed 3 years ago

ed513f85

doc(set_theory/cardinal/basic): tweak documentation (#15480)

vihdzp committed 3 years ago

a641e1b6

feat(algebra/order/monoid): add `one_lt_mul_iff`/`add_pos_iff` (#15458)

urkud committed 3 years ago

5c062ff9

Newer Older