leanprover-community/mathlib

Pull Requests Commits

same as the previous commit, but for curry

eric-wieser committed 3 years ago

832f3d71

more rfl proofs

eric-wieser committed 3 years ago

a96d3c4b

eric-wieser committed 3 years ago

35d74047

refactor(data/dfinsupp/basic): Improve definitional equalities of coercions

eric-wieser committed 3 years ago

e9e08778

feat(representation_theory/Action): mapping by a monoidal functor (#14331)

kim-em committed 3 years ago

1e72fb3f

feat(set_theory/zfc): `Ø ⊆ x` (#15223)

vihdzp committed 3 years ago

c70a787e

feat(topology/support): add lemmas, fix a name (#15484)

urkud committed 3 years ago

e1c8bded

feat(field_theory/adjoin): Compact elements of `intermediate_field` (#15438)

tb65536 committed 3 years ago

ebe60290

feat(analysis/calculus): generalize `differentiable*.pow`, add `differentiable*.zpow` (#15416)

urkud committed 3 years ago

150b8e81

feat(analysis/inner_product/calculus): [higher] differentiability to/from `euclidean_space` (#15363)

ADedecker committed 3 years ago

632b4970

refactor(set_theory/zfc): `Union` → `sUnion` (#15352)

vihdzp committed 3 years ago

58d7431d

feat(set_theory/zfc): `∈` is well-founded (#15213)

vihdzp committed 3 years ago

11576dbb

feat(topology/algebra/filter_basis): add a variant of `module_filter_basis.has_continuous_smul` when we already have a topological group (#14806)

ADedecker committed 3 years ago

d655f459

feat(algebra/category_theory/Group/epi_mono): about monomorphism and epimorphism in category of group (#14720)

jjaassoonn committed 3 years ago

45140211

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

Older