Commits leanprover-community/mathlib

feat(ring_theory/multiplicity): Equality of `factorization`, `multiplicity`, and `padic_val_nat` (#12033)

stuart-presnell committed 3 years ago

6e64492d

feat(topology/order/lattice): add a consequence of the continuity of sup/inf (#12003)

RemyDegenne committed 3 years ago

9307f5b4

feat(analysis/special_functions/complex/circle): `real.angle.exp_map_circle` lemmas (#11969)

jsm28 committed 3 years ago

60b77a76

feat(number_theory/zsqrtd/basic): add some lemmas (#11964)

Ruben-VandeVelde committed 3 years ago

0c33309c

feat(set_theory/ordinal_arithmetic): Suprema of functions with the same range are equal (#11910)

vihdzp committed 3 years ago

3d1354ce

refactor(set_theory/ordinal_arithmetic): `omin` → `Inf` (#11867)

vihdzp committed 3 years ago

721bace8

feat(model_theory/finitely_generated): Finitely generated and countably generated (sub)structures (#11857)

awainverse committed 3 years ago

9acc1d40

feat(data/nat/modeq): add modeq and dvd lemmas from Apostol Chapter 5 (#11787)

stuart-presnell committed 3 years ago

41dd6d8a

feat(topology/uniform/uniform_embedding): a sum of two complete spaces is complete (#11971)

sgouezel committed 3 years ago

b0508f3c

feat(order/category/Lattice): The category of lattices (#11968)

YaelDillies committed 3 years ago

77ca1ed3

feat(number_theory/cyclotomic/zeta): add lemmas (#11786)

riccardobrasca committed 3 years ago

5bcffd96

feat(order/complete_boolean_algebra): Frames (#11709)

YaelDillies committed 3 years ago

a2d7b55a

feat(topology/algebra/module/locally_convex): define locally convex spaces (#11859)

ADedecker committed 3 years ago

440e6b3b

feat(group_theory/nilpotent): products of nilpotent groups (#11827)

nomeata committed 3 years ago

c5578f91

feat(topology/algebra): weaken typeclasses to only require `has_continuous_const_smul` (#11995)

eric-wieser committed 3 years ago

f12b3d91

chore(category_theory/triangulated/rotate): optimizing some proofs (#12031)

arthurpaulino committed 3 years ago

f1334b95

chore(probability_theory/*): Rename folder (#11989)

YaelDillies committed 3 years ago

4c76eac9

chore(scripts): update nolints.txt (#12048)

leanprover-community-bot committed 3 years ago

430faa98

feat(analysis/inner_product_space/adjoint): `is_self_adjoint_iff_eq_a… (#12047)

hparshall committed 3 years ago

a1283d0b

feat(analysis/special_functions/complex/arg): `arg_coe_angle_eq_iff` (#12017)

jsm28 committed 3 years ago

92ac8ff8

chore(number_theory/padics/padic_norm): golf `prod_pow_prime_padic_val_nat` (#12034)

stuart-presnell committed 3 years ago

5dc720d1

chore(category_theory/linear/yoneda): Removing some slow uses of `obviously` (#11979)

stuart-presnell committed 3 years ago

f9bac45c

refactor(topology/constructions): turn `cofinite_topology` into a type synonym (#11967)

urkud committed 3 years ago

efdce094

feat(algebra/covariant_and_contravariant): covariance and monotonicity (#11815)

ecstatic-morse committed 3 years ago

ec11e5f5

doc(number_theory/cyclotomic/gal): fix typo (#12038)

ericrbg committed 3 years ago

4ba83349

feat(data/nat/factorization): add `le_of_mem_factorization` (#12032)

stuart-presnell committed 3 years ago

263833cf

chore(data/equiv/set): more lemmas about prod (#12022)

eric-wieser committed 3 years ago

1a3c0696

feat(data/list/big_operators): add `list.prod_map_mul` (#12029)

kmill committed 3 years ago

583ea58a

feat(algebra/star/self_adjoint): generalize scalar action instances (#12021)

eric-wieser committed 3 years ago

199e8ca8

feat(analysis/normed_space/linear_isometry): `trans_one`, `one_trans`, `refl_mul`, `mul_refl` (#12016)

jsm28 committed 3 years ago

5166aaab