leanprover-community/mathlib

Pull Requests Commits

Merge branch 'adomani_compute_degree_le' into adomani_poleq

adomani committed 3 years ago

8ca5525c

Merge remote-tracking branch 'origin/master' into adomani_compute_degree_le

adomani committed 3 years ago

58d66082

adomani committed 3 years ago

8af4c459

chore(set_theory/ordinal/basic): remove `rel_iso_out` (#15145)

vihdzp committed 3 years ago

bf735cd1

chore(*): add missing `to_fun → apply` configurations for `simps` (#15112)

eric-wieser committed 3 years ago

9b2755b9

chore(data/nat): rename oddly named lemma odd_gt_zero (#13040)

alexjbest committed 3 years ago

ab99fd1b

adomani committed 3 years ago

3bc841c5

adomani committed 3 years ago

3c525d2b

feat(order/lattice, order/lattice_intervals): coe inf/sup lemmas (#15136)

apnelson1 committed 3 years ago

6d02dac3

feat(combinatorics/simple_graph/basic): `dart.to_prod` is injective (#15150)

kmill committed 3 years ago

418373e8

feat(data/quot): `is_equiv` instance for quotient equivalence (#15148)

vihdzp committed 3 years ago

3e52000c

feat(order/rel_iso): add `rel_iso.cast` (#15144)

vihdzp committed 3 years ago

e034eb09

refactor(group_theory/congruence): use `quotient.map` (#15130)

urkud committed 3 years ago

e335a41f

feat(measure_theory/integral): Circle integral transform (#13885)

CBirkbeck committed 3 years ago

fdfc2229

chore(set_theory/ordinal/basic): clean up `ordinal.card` API (#15147)

vihdzp committed 3 years ago

0a89f18f

feat(set_theory/ordinal/basic): basic lemmas on `ordinal.lift` (#15146)

vihdzp committed 3 years ago

a54e63da

feat(order/basic): a symmetric relation implies equality when it implies less-equal (#15149)

vihdzp committed 3 years ago

b7581040

refactor(topology/separation): redefine `t0_space` (#15046)

urkud committed 3 years ago

d45a8ace

feat(analysis/inner_product_space): add simple lemmas for the orthogonal complement (#15020)

mcdoll committed 3 years ago

71b1be63

feat(geometry/manifold/local_invariant_properties): simplify definitions and proofs (#15116)

fpvandoorn committed 3 years ago

f09322bc

feat(analysis/special_functions/complex/arg): add complex.abs_eq_one_iff (#15125)

Ruben-VandeVelde committed 3 years ago

8ff5e113

chore(data/fintype): drop a `decidable_pred` assumption (#14971)

urkud committed 3 years ago

d908bc0b

feat(probability/martingale): Doob's maximal inequality (#14737)

kex-y committed 3 years ago

a95b4427

doc(overview): add probability theory (#15114)

fpvandoorn committed 3 years ago

bd9c307d

feat(analysis/convex/function): Variants of `convex_on.le_right_of_left_le` (#14821)

tb65536 committed 3 years ago

93e97d1e

chore(analysis/normed/field/basic): add `@[simp]` to `real.norm_eq_abs (#15006)

urkud committed 3 years ago

71e11de8

feat(probability/martingale): positive part of a submartingale is also a submartingale (#14932)

kex-y committed 3 years ago

071dc908

feat(*): add lemmas about sigma types (#15085)

urkud committed 3 years ago

f10d0abc

feat(topology/sets/compacts): prod constructions (#15118)

sgouezel committed 3 years ago

527afb3d

feat(analysis/complex): equiv_real_prod_symm_apply (#15122)

sgouezel committed 3 years ago

db9cb466

Older