leanprover-community/mathlib3

Pull Requests Commits

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

feat(number_theory/padics/padic_val): add `padic_val_nat_def'` and generalise `pow_padic_val_nat_dvd` (#14637)

stuart-presnell committed 3 years ago

c0b3ed79

refactor(group_theory/sylow): Golf proof of `pow_dvd_card_of_pow_dvd_card` (#14622)

tb65536 committed 3 years ago

dc766dd4

feat(analysis/seminorm): removed unnecessary `norm_one_class` arguments (#14614)

eric-wieser committed 3 years ago

cde6e632

refactor(logic/equiv/basic): remove `fin_equiv_subtype` (#14603)

vihdzp committed 3 years ago

d997baa4

feat(algebra/module/torsion.lean): various lemmas about torsion modules (#14573)

pbazin committed 3 years ago

c2bb59e5

feat(combinatorics/ballot): the Ballot problem (#13592)

kex-y committed 3 years ago

dfc54a3a

feat(ring_theory/unique_factorization_domain): add some lemmas about … (#14555)

Ruben-VandeVelde committed 3 years ago

d51aacbd

chore(topology/metric_space): remove instances that duplicate lemmas (#14639)

eric-wieser committed 3 years ago

dc2f6bb9

feat(topology/metric_space/basic): add lemma `exists_lt_mem_ball_of_mem_ball` (#14627)

ocfnash committed 3 years ago

bc7b3425

feat(analysis/seminorm): add a `zero_hom_class` instance and remove `seminorm.zero` (#14613)

eric-wieser committed 3 years ago

6a1ce4e8

doc(data/vector3): improve wording (#14610)

vihdzp committed 3 years ago

6826bf00

Newer Older