leanprover-community/mathlib3

Pull Requests Commits

feat(logic/equiv/local_equiv): add 2 lemmas (#15611)

urkud committed 3 years ago

1a73c7ee

feat(topology/algebra/module/finite_dimension): add 2 simp lemmas (#15610)

urkud committed 3 years ago

80d79069

chore(ring_theory/localization/basic): golf sec_snd_ne_zero (#15572)

Multramate committed 3 years ago

716616b3

chore(set_theory/ordinal/arithmetic): change `0 < x` assumptions to `x ≠ 0` (#15562)

vihdzp committed 3 years ago

4b82074e

feat(algebraic_geometry/AffineScheme): Affine communication lemma (#15487)

erdOne committed 3 years ago

ac9e3583

chore(set_theory/game/nim): review `simp` lemmas (#15407)

vihdzp committed 3 years ago

30edc932

feat(topology/instances/ennreal): add `continuous(_on).ennreal_mul` (#15593)

urkud committed 3 years ago

68451363

feat(data/set/intervals): add lemmas (#15608)

urkud committed 3 years ago

4d5ac734

feat(data/set/prod): add theorems about `λ x, (x, x)` (#15604)

urkud committed 3 years ago

98c62bd0

feat(integration): elementary version of FTC-1 (#15603)

PatrickMassot committed 3 years ago

e52026f7

chore(ring_theory/polynomial/symmetric): golf (#15598)

urkud committed 3 years ago

bd4a574f

docs(undergrad): add pointwise convergence (#15601)

PatrickMassot committed 3 years ago

e27e99b9

docs(undergrad): clean up distribution section (#15600)

PatrickMassot committed 3 years ago

2f99fd41

docs(undergrad): add polar integration (#15597)

PatrickMassot committed 3 years ago

d96fc102

refactor(data/list/chain): `transitive` → `is_trans` on `chain.pairwise` (#15571)

vihdzp committed 3 years ago

c97887bd

feat(analysis/calculus/cont_diff): generalize `mul` lemmas to a normed algebra (#15595)

urkud committed 3 years ago

d98479aa

doc(number_theory/bernoulli_polynomials): a few small improvements (#15599)

alexjbest committed 3 years ago

91416440

feat(order/succ_pred/limit): Successor and predecessor limits (#15001)

vihdzp committed 3 years ago

767aeb39

feat(order/initial_seg): Initial/principal segment from empty type (#15375)

vihdzp committed 3 years ago

9bf23b0a

feat(data/real/basic): add a repr showing an underlying cauchy sequence (#15575)

eric-wieser committed 3 years ago

d749b205

feat(linear_algebra/linear_pmap): more lemmas about the graph (#15531)

mcdoll committed 3 years ago

c0c910de

chore(data/real/basic,number_theory/padics/padic_numbers): eliminate `real.of_rat` and `padic.of_rat` (#15569)

eric-wieser committed 3 years ago

591992d7

feat(topology/partition_of_unity): local to global (#15490)

urkud committed 3 years ago

7f16dd20

refactor(set_theory/zfc): make `Class` morally `Set → Prop` (#15248)

vihdzp committed 3 years ago

f05fdcac

feat(set_theory/cardinal/ordinal): basic properties on Beth numbers (#14989)

vihdzp committed 3 years ago

99625b1b

feat(algebraic_topology/dold_kan): technical lemmas about face maps (#14044)

joelriou committed 3 years ago

d29aca84

doc(data/dfinsupp): improve the docstring for dfinsupp (#15554)

eric-wieser committed 3 years ago

72e0e9a5

feat(set_theory/zfc/ordinal): more lemmas on transitive sets (#15548)

vihdzp committed 3 years ago

8672734e

fix(data/set_like): `coe_sort_trans` should have low priority (#15489)

Vierkantor committed 3 years ago

8983bec7

refactor(field_theory/*): Refactor `normal` to use `is_algebraic` (#15421)

tb65536 committed 3 years ago

62b5bb74

Newer Older