leanprover-community/mathlib3

Pull Requests Commits

Attempt to use is_freely_generated_by in nielsen_schreier, but probbly misguided

nomeata committed 3 years ago

584ff52d

elab_simple to the rescue

nomeata committed 3 years ago

e3c8b7d4

Try to use out_param

nomeata committed 3 years ago

881f9693

At least no sorry

nomeata committed 3 years ago

14562388

Try to use then new API

nomeata committed 3 years ago

de9241d0

nomeata committed 3 years ago

02124a67

Draft the is_freely_generated_by API

nomeata committed 3 years ago

939c9b98

feat(analysis/convex): golf some proofs (#13451)

urkud committed 3 years ago

e6322c6a

feat(data/fin/tuple/nat_antidiagonal): add `list.nat.antidiagonal_tuple_pairwise_pi_lex` (#13339)

eric-wieser committed 3 years ago

b90e770f

chore(algebra/big_operators/fin): moving lemmas (#13331)

joelriou committed 3 years ago

9380977b

feat(topology/[separation, homeomorph]): separation properties are topological invariants (#13401)

ADedecker committed 3 years ago

7c7f3514

feat(topology/algebra/order): extreme value thm for a function continuous on a closed set (#13348)

urkud committed 3 years ago

49e41eb5

chore(scripts): update nolints.txt (#13482)

leanprover-community-bot committed 3 years ago

f4f46cd5

feat(data/finsupp/basic): add a few lemmas, mostly about `finsupp.filter` (#13457)

urkud committed 3 years ago

d4fda045

chore(number_theory/*): Weaken assumptions (#13443)

YaelDillies committed 3 years ago

96667b51

chore(order/bounded_order): Match the `with_bot` and `with_top` API (#13419)

YaelDillies committed 3 years ago

018e9b57

chore(logic/encodable/basic): Rename `encodable` instances (#13396)

YaelDillies committed 3 years ago

8decd4b1

feat(algebra/order/monoid): Co/contravariant classes for `with_bot`/`with_top` (#13369)

YaelDillies committed 3 years ago

91a43e71

feat(data/polynomial/eval): generalize smul lemmas (#13479)

astrainfinita committed 3 years ago

874dde52

feat(data/polynomial/taylor): add `taylor_alg_hom` (#13477)

astrainfinita committed 3 years ago

010f09e7

feat(data/polynomial/eval): add `protected` on some lemmas about `polynomial.map` (#13478)

astrainfinita committed 3 years ago

f7430cd7

feat(topology/stone_cech): add stone_cech_hom_ext (#13472)

mapehe committed 3 years ago

862a5854

feat(algebraic_topology/fundamental_groupoid/fundamental_group): add type checker helpers for convertings paths to/from elements of fundamental group (#13182)

mlavrent committed 3 years ago

449e06a9

chore(number_theory/function_field): fix typo (#13464)

mariainesdff committed 3 years ago

c988c622

refactor(number_theory/legendre_symbol/): move Gauss/Eisenstein lemma code to separate file (#13449)

MichaelStollBayreuth committed 3 years ago

fbff76b5

feat(data/sym/sym2): mem_map/mem_congr/map_id' (#13437)

kmill committed 3 years ago

0c2d68a0

feat(analysis/normed_space/pointwise): Balls disjointness (#13379)

YaelDillies committed 3 years ago

d6c1cf16

chore(ring_theory/ideal/local_ring): generalize to semirings (#13341)

yuma-mizuno committed 3 years ago

2194eef2

feat(number_theory/padics/padic_numbers): add padic.add_valuation (#12939)

mariainesdff committed 3 years ago

c65bebb5

chore(*): clean up unnecessary uses of nat.cases_on (#13454)

alexjbest committed 3 years ago

bbbea1c1

Older