Commits leanprover-community/mathlib3

feat(order/basic): More order instances for `subtype` (#13134)

YaelDillies committed 3 years ago

7ba9c3fe

feat(algebraic_geometry/projective_spectrum): structure sheaf of Proj of graded ring (#13072)

jjaassoonn committed 3 years ago

0453d606

feat(analysis/normed/normed_field): Pi types form a normed ring (#12912)

eric-wieser committed 3 years ago

f94cd0f1

feat(data/fin/tuple/nat_antidiagonal): add an equiv and some TODO comments. (#13338)

eric-wieser committed 3 years ago

887f9338

chore(representation_theory/invariants): clean up some simps (#13337)

Ruben-VandeVelde committed 3 years ago

455bc657

feat(category_theory/fully_faithful): nat_trans_of_comp_fully_faithful (#13327)

kim-em committed 3 years ago

e8339bd6

chore(*): remove numerous edge cases from lemmas (#13316)

alexjbest committed 3 years ago

4a070542

feat(number_theory/quadratic_reciprocity): change order of arguments … (#13311)

MichaelStollBayreuth committed 3 years ago

a839f4dc

feat(probability/integration): characterize indep_fun by expected product of comp (#13270)

vbeffara committed 3 years ago

4e1102a0

feat(data/set/basic): Missing `set.image_perm` (#13242)

MantasBaksys committed 3 years ago

a521a32e

feat(computability/*): Automata lemmas (#13194)

YaelDillies committed 3 years ago

dee49588

feat(number_theory/cyclotomic/primitive_roots): add `pow_sub_one_norm_prime_pow_ne_two` (#13152)

riccardobrasca committed 3 years ago

77ae0912

feat(measure_theory/measure/haar): Add the Steinhaus Theorem (#12932)

MantasBaksys committed 3 years ago

04250c8d

feat(data/sign): the sign function (#12835)

ericrbg committed 3 years ago

cea5e4bb

feat(combinatorics/simple_graph/connectivity): induced maps on walks and paths (#13310)

kmill committed 3 years ago

695a2b69

chore(category_theory/*): reduce imports (#13305)

kim-em committed 3 years ago

a447dae9

feat(combinatorics/simple_graph/{connectivity,adj_matrix}): powers of adjacency matrix (#13304)

kmill committed 3 years ago

5e8d6bb3

chore(category_theory): switch ulift and filtered in import hierarchy (#13302)

kim-em committed 3 years ago

bfd53845

feat(measure_theory/function/uniform_integrable): Equivalent condition for uniformly integrable in the probability sense (#12955)

kex-y committed 3 years ago

dcb6c865

feat(ring_theory/coprime/lemmas): alternative characterisations of pairwise coprimeness (#12911)

pbazin committed 3 years ago

797c7133

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