Commits leanprover-community/mathlib

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

refactor(algebra/sub{monoid,group,ring,semiring,field}): merge together the `restrict` and `cod_restrict` helpers (#14548)

eric-wieser committed 3 years ago

ab64f631

feat(order/compactly_generated): an independent subset of a well-founded complete lattice is finite (#14215)

ocfnash committed 3 years ago

732b79f8

feat(algebra/order/monoid): `zero_le_one_class` instances for `with_top` and `with_bot` (#14640)

vihdzp committed 3 years ago

3a95d1d3

feat(logic/equiv/basic): two empty types are equivalent; remove various redundant lemmas (#14604)

vihdzp committed 3 years ago

971a9b00

feat(logic/small): generalize + golf (#14584)

vihdzp committed 3 years ago

9f19686c

feat(data/nat/factorization/basic): two trivial simp lemmas about factorizations (#14634)

stuart-presnell committed 3 years ago

b392bb2c