leanprover-community/mathlib

Pull Requests Commits

fix linter error

jjaassoonn committed 3 years ago

c4df7570

jjaassoonn committed 3 years ago

d789db28

Merge branch 'jjaassoonn/coextension' of https://github.com/leanprover-community/mathlib into jjaassoonn/coextension

jjaassoonn committed 3 years ago

ce7822e0

slight golf and fix

jjaassoonn committed 3 years ago

7e58a21a

Update adjunctions.lean

jjaassoonn committed 3 years ago

Verified 46ea128a

add one more extension

jjaassoonn committed 3 years ago

b34ae182

apply suggestion from code review

jjaassoonn committed 3 years ago

70cfdf10

jjaassoonn committed 3 years ago

7fcfe4d7

refactor(group_theory/group_action/basic): Make `mul_action.self_equiv_sigma_orbits` computable (#14591)

eric-wieser committed 3 years ago

3527e4ad

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

Older