Commits leanprover-community/mathlib3

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

refactor(data/finset/nat_antidiagonal): state lemmas with cons instead of insert (#14533)

eric-wieser committed 3 years ago

4fc35392

chore(data/set/basic): minor style fixes (#14628)

vihdzp committed 3 years ago

0c08bd43

feat(linear_algebra/affine_space/affine_subspace/pointwise): Translations are an action on affine subspaces (#14230)

winston-h-zhang committed 3 years ago

c1faa2ee

refactor(topology/metric_space/basic): add `pseudo_metric_space.to_bornology'` (#13927)

urkud committed 3 years ago

84a1bd6a

feat(set_theory/ordinal/basic): tweak `type_def` + golf `type_lt` (#14611)

vihdzp committed 3 years ago

61df9c66

feat(ring_theory/valuation/valuation_subring): define unit group of valuation subring and provide basic API (#14540)

mckoen committed 3 years ago

9c4a3d1b

feat(model_theory/substructures): tweak universes for `lift_card_closure_le` (#14597)

vihdzp committed 3 years ago

d3156667

feat(set_theory/ordinal/basic): `rel_iso.ordinal_type_eq` (#14602)

vihdzp committed 3 years ago

89348848

feat(order/rel_classes): any relation on an empty type is a well-order (#14600)

vihdzp committed 3 years ago

09df85f6

chore(*): remove extra parentheses in universe annotations (#14595)

vihdzp committed 3 years ago

201a3f4a

feat(algebra/algebra/basic): add instances `char_zero.no_zero_smul_divisors_int`, `char_zero.no_zero_smul_divisors_nat` (#14395)

ocfnash committed 3 years ago

3e4d6aa3

feat(logic/basic): add lemma `pi_congr` (#14616)

adomani committed 3 years ago

bfb8ec83

refactor(algebra/is_prime_pow): move lemmas using `factorization` to new file (#14598)

stuart-presnell committed 3 years ago

700181a3