leanprover-community/mathlib3

Pull Requests Commits

AlexKontorovich committed 3 years ago

2fa215d1

feat(topology/uniform_space/equiv): define uniform isomorphisms (#14537)

ADedecker committed 3 years ago

18936e55

feat(topology/algebra/order): `coe : ℚ → 𝕜` has dense range (#14635)

urkud committed 3 years ago

8c812fd4

feat(data/rat): Add some lemmas to work with num/denom (#14456)

Jon Eugster committed 3 years ago

0f5a1f22

feat(analysis/inner_product_space): Generalize Gram-Schmidt (#14379)

abentkamp committed 3 years ago

95da6493

feat(set_theory/game/ordinal): golf `to_pgame_injective` (#14661)

vihdzp committed 3 years ago

391d1780

refactor(set_theory/game/pgame): rename and add theorems like `-y ≤ -x ↔ x ≤ y` (#14653)

vihdzp committed 3 years ago

68dc07f6

feat(data/fintype/basic): add `card_subtype_mono` (#14645)

linesthatinterlace committed 3 years ago

a9123922

chore(topology/metric_space/basic): add `metric_space.replace_bornology` (#14638)

eric-wieser committed 3 years ago

771f2b7b

refactor(logic/equiv/basic): tweak lemmas on equivalences between `unique` types (#14605)

vihdzp committed 3 years ago

5bccb515

feat(data/polynomial/derivative): reduce assumptions (#14338)

astrainfinita committed 3 years ago

76918216

feat(dynamics/periodic_pts): Orbit under periodic function (#12976)

vihdzp committed 3 years ago

39184f40

feat(data/finite/basic): `finite` predicate (#14373)

kmill committed 3 years ago

e3dade35

chore(measure_theory): golf (#14657)

urkud committed 3 years ago

e9d25648

feat(set_theory/ordinal/basic): tweak theorems on order type of empty relation (#14650)

vihdzp committed 3 years ago

ed2cfce8

chore(analysis/special_functions/gamma): tidy some proofs (#14615)

Ruben-VandeVelde committed 3 years ago

2cf4746b

feat(ci): Add support for "notice"-level messages (#14443)

eric-wieser committed 3 years ago

3afb1fa1

feat(set_theory/ordinal/basic): better definitions for `0` and `1` (#14651)

vihdzp committed 3 years ago

6e136177

feat(set_theory/cardinal): add `cardinal.aleph_0_le_mul_iff'` (#14648)

urkud committed 3 years ago

c89d3194

feat(data/matrix): Lemmas about `vec_mul`, `mul_vec`, `dot_product`, `inv` (#14644)

abentkamp committed 3 years ago

405be36f

chore(topology/sequences): rename variables (#14631)

urkud committed 3 years ago

3e458e23

chore(set_theory/cardinal/basic): tidy lt_wf proof (#14574)

Ruben-VandeVelde committed 3 years ago

81ab992e

feat(algebra/order/ring): Binary rearrangement inequality (#14478)

YaelDillies committed 3 years ago

34a9d0df

feat(data/nat/choose/central): arity of primes in central binomial coefficients (#14017)

BoltonBailey committed 3 years ago

7fbff0f7

chore(ring_theory/unique_factorization_domain): drop simp annotation for factors_pow (#14646)

Ruben-VandeVelde committed 3 years ago

4d4de43e

feat(analysis/inner_product_space/pi_L2): Distance formula in the euclidean space (#14642)

YaelDillies committed 3 years ago

7b4680fe

feat(special_functions/integrals): exponential of complex multiple of x (#14623)

loefflerd committed 3 years ago

ac0ce64c

feat(data/set/intervals): add lemmas about unions of intervals (#14636)

urkud committed 3 years ago

abee6498

feat(topology/constructions): add `subtype.dense_iff` (#14632)

urkud committed 3 years ago

e0f3ea31

chore(analysis/convex/integral): use `variables` (#14592)

urkud committed 3 years ago

48f557d5

Older