Commits leanprover-community/mathlib3

Merge remote-tracking branch 'origin/master' into eric-wieser/stars-and-bars

eric-wieser committed 3 years ago

1f085806

feat(data/option/basic): add `option.coe_get` (#13081)

stuart-presnell committed 3 years ago

67d60972

refactor(category_theory/differential_object): simp only -> simp_rw (#13333)

kim-em committed 3 years ago

41398242

chore(category_theory/monoidal/discrete): typo in to_additive name (#13332)

kim-em committed 3 years ago

c7e76bc8

feat(analysis/complex/re_im_topology): add `metric.bounded.re_prod_im` (#13324)

urkud committed 3 years ago

d4059557

feat(measure_theory/constructions/borel_space): a set with `μ (∂ s) = 0` is null measurable (#13322)

urkud committed 3 years ago

ebbe763f

feat(order/conditionally_complete_lattice): Make `cSup_empty` a `simp` lemma (#13318)

vihdzp committed 3 years ago

7e69148c

feat(set_theory/ordinal_arithmetic): `is_normal.monotone` (#13314)

vihdzp committed 3 years ago

159855d1

doc(combinatorics/simple_graph/basic): mention half-edge synonym for darts (#13312)

kmill committed 3 years ago

c5b83f0a

feat(category_theory/nat_iso): add simp lemmas (#13303)

kim-em committed 3 years ago

722c0dfa

feat(analysis/special_functions/pow): `z ^ w` is continuous in `(z, w)` at `(0, w)` if `0 < re w` (#13288)

urkud committed 3 years ago

f7e862f6

feat(data/complex/is_R_or_C): add `polynomial.of_real_eval` (#13287)

urkud committed 3 years ago

57682ffa

feat(analysis/asymptotics): add a few versions of `c=o(x)` as `x→∞` (#13286)

urkud committed 3 years ago

577df07c

feat(group_theory/group_action/basic): A `quotient_action` induces an action on left cosets (#13283)

tb65536 committed 3 years ago

171e2aa2

feat(group_theory/transversal): A `quotient_action` induces an action on left transversals (#13282)

tb65536 committed 3 years ago

65b5dd8b

chore(topology/algebra/uniform_group): use morphism classes (#13273)

ADedecker committed 3 years ago

2eba5241

feat(topology/order): if `e` is an equiv, `induced e.symm = coinduced e` (#13272)

ADedecker committed 3 years ago

2b80d4a0

feat(algebra/big_operators): `norm_num` plugin for list/multiset/finset prod/sum (#13005)

Vierkantor committed 3 years ago

c1600832

feat(scripts): make style lint script more robust to lines starting with spaces (#13317)

alexjbest committed 3 years ago

e5bd9413

feat(analysis/special_functions/pow): more versions of `x ^ k = o(exp(b * x))` (#13285)

urkud committed 3 years ago

cd616e0d

fix(algebra/indicator_function): fix name of `mul_indicator_eq_one_iff` (#13284)

urkud committed 3 years ago

706905c5

feat(model_theory/basic): Structures over the empty language (#13281)

awainverse committed 3 years ago

ff507a35

feat(topology/algebra/uniform_group): a subgroup of a uniform group is a uniform group (#13277)

ADedecker committed 3 years ago

fe17fee1

feat(group_theory/schreier): Finset version of Schreier's lemma (#13274)

tb65536 committed 3 years ago

6f428ed4

fix(algebra/module/basic,group_theory/group_action/defs): generalize nat and int smul_comm_class instances (#13174)

eric-wieser committed 3 years ago

102311e6

refactor(order/conditionally_complete_lattice): `csupr_le_csupr` → `csupr_mono` (#13320)

vihdzp committed 3 years ago

4d27ecf7

chore(*): make more transitive relations available to calc (#12860)

ericrbg committed 3 years ago

6f9cb03e

chore(measure_theory/mconstructions/prod): Speed up `finite_spanning_sets_in.prod` (#13325)

YaelDillies committed 3 years ago

a85958cf

feat(topology/algebra/order): add `le_on_closure` (#13290)

urkud committed 3 years ago

a2d09b24

chore(topology/uniform_space/basic): golf a proof (#13289)

urkud committed 3 years ago

e5ae0991