Commits leanprover-community/mathlib3

feat(algebra/big_operators/finprod): add finprod.mem_dvd (#9549)

mariainesdff committed 4 years ago

845d064a

move(data/fin/*): group `fin` files under a `fin` folder (#9524)

YaelDillies committed 4 years ago

b2ae1956

feat(analysis/normed_space/add_torsor_bases): barycentric coordinates are open maps (in finite dimensions over a complete field) (#9543)

ocfnash committed 4 years ago

5c3cdd21

fix(computability/DFA): tighten regular pumping lemma to match standard textbooks (#9585)

dupuisf committed 4 years ago

a7b4e782

refactor(data/equiv): split out `./set` from `./basic` (#9560)

eric-wieser committed 4 years ago

bcd13a77

feat(analysis/normed_space/banach): open mapping theorem for maps between affine spaces (#9540)

ocfnash committed 4 years ago

0b356b00

feat(group_theory/group_action/conj_act): conjugation action of groups (#8627)

ChrisHughes24 committed 4 years ago

5773bc63

chore(ring_theory/witt_vector): fix a docstring (#9575)

jcommelin committed 4 years ago

6abd6f2d

feat(analysis/convex/function): Dual lemmas (#9571)

YaelDillies committed 4 years ago

850d5d28

refactor(data/nat/basic): remove sub lemmas (#9544)

fpvandoorn committed 4 years ago

8c657818

feat(topology/algebra): topology on a linear_ordered_comm_group_with_zero (#9537)

PatrickMassot committed 4 years ago

facc1d2d

refactor(analysis/{normed_space, inner_product_space}/dual): redefine using `linear_isometry` (#9569)

hrmacbeth committed 4 years ago

b534feda

feat(order/bounds): Antitone lemmas (#9556)

YaelDillies committed 4 years ago

e52e5338

feat(linear_algebra/affine_space/barycentric_coords): barycentric coordinates are 1 in zero dimensions (#9564)

ocfnash committed 4 years ago

f811910b

chore(linear_algebra/quadratic_form): squeeze simps (#9572)

fpvandoorn committed 4 years ago

db5ee760

feat(topology/bases): a family of nonempty disjoint open sets is countable in a separable space (#9557)

sgouezel committed 4 years ago

fdf8a71f

feat(analysis/normed_space/affine_isometry): affine maps are open iff their underlying linear maps are (#9538)

ocfnash committed 4 years ago

815eaca0

doc(linear_algebra/free_module/strong_rank_condition): correct a typo (#9565)

riccardobrasca committed 4 years ago

63903f27

feat(order/bounds): Image under an `order_iso` and `upper_bounds` commute (#9555)

YaelDillies committed 4 years ago

0b575206

feat(data/int/interval): Finite intervals in ℤ (#9526)

YaelDillies committed 4 years ago

111d73bf

chore(linear_algebra/quadratic_form): speed up quadratic_form.lin_mul_lin (#9567)

Ruben-VandeVelde committed 4 years ago

7455f47c

fix(data/equiv/basic): use `subtype p` not `coe_sort (set_of p)` (#9559)

eric-wieser committed 4 years ago

5926f103

chore(measure_theory/*): better names and notations, add easy lemmas (#9554)

sgouezel committed 4 years ago

da4d5501

feat(analysis/convex/basic): Levels of a monotone/antitone function (#9547)

YaelDillies committed 4 years ago

e7ea02fd

feat(ring_theory/polynomial/basic): add a lemma `polynomial_quotient_equiv_quotient_polynomial_map_mk` (#9542)

Paul-Lez committed 4 years ago

5b793197

refactor(algebra/gcd_monoid): don't require normalization (#9443)

Ruben-VandeVelde committed 4 years ago

26660331

refactor(topology/algebra/module): continuous semilinear maps (#9539)

dupuisf committed 4 years ago

def4814c

refactor(analysis/convex/*): prove `convex_independent_iff_finset` without full Carathéodory (#9550)

YaelDillies committed 4 years ago

fefd8a38

feat(topology/algebra): adic topology (#9521)

PatrickMassot committed 4 years ago

c42786f5

ci(.github/workflows): automatically remove awaiting-CI label (#9491)

bryangingechen committed 4 years ago

61cd266a