Commits leanprover-community/mathlib

chore(topology/continuous_on): fix a typo (#11190)

urkud committed 4 years ago

03a54829

feat(ring_theory/algebraic): algebraic functions (#11156)

pechersky committed 4 years ago

3f777613

feat(topology/algebra/ordered): new lemmas, update (#11184)

urkud committed 4 years ago

ebdbe6b0

chore(measure_theory): fix TC assumptions in 2 lemmas (#11185)

urkud committed 4 years ago

02d02dfc

feat(topology/metric_space/basic): add `fin.dist_insert_nth_insert_nth` (#11183)

urkud committed 4 years ago

c1b10417

chore(order/rel_classes): Removed unnecessary `classical` (#11180)

vihdzp committed 4 years ago

6486e9b3

feat(algebraic_geometry/*): The map `F.stalk y ⟶ F.stalk x` for `x ⤳ y` (#11144)

erdOne committed 4 years ago

93cf56c5

feat(linear_algebra/multilinear/basic): the space of multilinear maps is finite-dimensional when the components are finite-dimensional (#10504)

ocfnash committed 4 years ago

892d465a

feat(combinatorics/configuration): Line count equals point count (#11169)

tb65536 committed 4 years ago

53533697

feat(group_theory/specific_groups/*): computes the exponents of the dihedral and generalised quaternion groups (#11166)

Julian-Kuelshammer committed 4 years ago

a6c82afb

feat(data/nat/log): log_mul, log_div (#11164)

pechersky committed 4 years ago

ad76a5ee

feat(algebraic_geometry): The function field of an integral scheme (#11147)

erdOne committed 4 years ago

23b01cc4

feat(normed_space/lp_space): Lp space for `Π i, E i` (#11015)

hrmacbeth committed 4 years ago

1594b0ca

feat(data/set/*): lemmas about `monotone`/`antitone` and sets/intervals (#11173)

urkud committed 4 years ago

742ec88c

fix(order/filter/ultrafilter): dedup instance names (#11171)

kbuzzard committed 4 years ago

979f2e72

feat(combinatorics/simple_graph/srg): is_SRG_with for complete graphs, edgeless graphs, and complements (#5698)

agusakov committed 4 years ago

da54388a

chore(category_theory/closed/cartesian): make exp right-associative (#11172)

dwarn committed 4 years ago

8db2fa05

feat(data/quot): Add quotient pi induction (#11137)

prakol16 committed 4 years ago

559951cd

feat(analysis/normed_space/banach_steinhaus): prove the standard Banach-Steinhaus theorem (#10663)

j-loreaux committed 4 years ago

200f47d3

feat(data/polynomial/ring_division): golf and generalize `leading_coeff_div_by_monic_of_monic` (#11077)

pechersky committed 4 years ago

ea710ca6

feat(data/int/gcd): add theorem `gcd_least_linear` (#10743)

stuart-presnell committed 4 years ago

8ec59f9c

chore(data/sym/basic): golf and add missing simp lemmas (#11160)

eric-wieser committed 4 years ago

e4607f8f

feat(algebra/star/self_adjoint): define the self-adjoint elements of a star additive group (#11135)

dupuisf committed 4 years ago

fbbbdfa0

feat(data/polynomial/degree/lemmas): (nat_)degree_sum_eq_of_disjoint (#11121)

pechersky committed 4 years ago

fdf09df0

feat(linear_algebra/multilinear/basic): add dependent version of `multilinear_map.dom_dom_congr_linear_equiv` (#10474)

ocfnash committed 4 years ago

c4caf0ee

feat(data/list/indexes): map_with_index_eq_of_fn (#11163)

pechersky committed 4 years ago

9a38c196

chore(data/equiv/basic): missing dsimp lemmas (#11159)

eric-wieser committed 4 years ago

b92afc90

feat(category_theory/sites/plus): Adds a functorial version of `J.diagram P`, functorial in `P`. (#11155)

adamtopaz committed 4 years ago

bcf1d2dd

feat(category_theory/limits/functor_category): Some additional isomorphisms involving (co)limits of functors. (#11152)

adamtopaz committed 4 years ago

7b387924

feat(data/list/count): add lemma `count_le_count_map` (#11148)

stuart-presnell committed 4 years ago

b142b697