leanprover-community/mathlib

Pull Requests Commits

feat(topology/algebra/group): quotient by a closed subgroup is regular (#13278)

ADedecker committed 3 years ago

7be21e09

feat(order/chain): Flags (#13089)

YaelDillies committed 3 years ago

ad3e6672

feat(data/int/basic): Add unit lemmas (#13565)

tb65536 committed 3 years ago

9c3cb72c

feat(analysis/convex/strict_convex_space): Verify strict convexity from fixed scalars (#13548)

YaelDillies committed 3 years ago

695e0b70

feat(topology/metric_space/hausdorff_distance): Thickening the closure (#13515)

YaelDillies committed 3 years ago

2e83d617

chore(ring_theory/roots_of_unity): primitive roots are not zero (#13587)

ericrbg committed 3 years ago

355d68ab

chore(data/polynomial/degree/definitions): simplify sum_fin, degree_C_le (#13564)

Ruben-VandeVelde committed 3 years ago

79ac4c81

feat(number_theory/legendre_symbol): add file quadratic_char.lean (#13503)

MichaelStollBayreuth committed 3 years ago

a74df9b5

chore(data/rat/basic): tidy some proofs (#13603)

Ruben-VandeVelde committed 3 years ago

631890bf

feat(logic/basic): add `auto_param.out` and `opt_param.out` (#13599)

urkud committed 3 years ago

f7dac5ea

feat(set_theory/game/pgame): simp + private (#13596)

vihdzp committed 3 years ago

6729cca2

refactor(data/nat/factorization): Infer arguments (#13595)

vihdzp committed 3 years ago

62205c27

chore(analysis/inner_product_space/lax_milgram): tidy some proofs (#13604)

Ruben-VandeVelde committed 3 years ago

9abfff39

feat(algebra/ring/basic): define non-unital ring homs (#13430)

j-loreaux committed 3 years ago

3d24b093

feat(order/filter/small_sets): define the filter of small sets (#13467)

fpvandoorn committed 3 years ago

394dec32

fix(data/fintype/basic): fix `fintype_of_option_equiv` (#13466)

stuart-presnell committed 3 years ago

9db59165

feat(analysis/calculus/specific_functions): define normed bump functions (#13463)

fpvandoorn committed 3 years ago

0d77f29f

feat(analysis/normed_space/exponential): Weaken typeclass requirements (#13444)

eric-wieser committed 3 years ago

06a6044f

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

leanprover-community-bot committed 3 years ago

2b902eb3

feat(data/mv_polynomial/equiv): API for `mv_polynomial.fin_succ_equiv` (#10812)

isadofschi committed 3 years ago

79bc6ad4

feat(polynomial/cyclotomic): `eval_apply` (#13586)

ericrbg committed 3 years ago

17d24243

feat(data/quot): `quotient.out` is injective (#13584)

vihdzp committed 3 years ago

40fc58cb

doc(category_theory/limits/has_limits): fix two docstrings (#13581)

jcommelin committed 3 years ago

821e7c89

chore(set_theory/cardinal/basic): Fix spacing (#13562)

vihdzp committed 3 years ago

7b92db75

fix(analysis/normed_space/basic): allow the zero ring to be a normed algebra (#13544)

eric-wieser committed 3 years ago

1da12b57

refactor(category_theory): make has_zero_object a Prop (#13517)

jcommelin committed 3 years ago

77236cd2

feat(group_theory/group_action/basic): Right multiplication satisfies the `quotient_action` axiom (#13475)

tb65536 committed 3 years ago

dced1336

chore(*): remove `subst` when not necessary (#13453)

ericrbg committed 3 years ago

bb9d1c50

feat(linear_algebra/prod): two lemmas about prod_map (#13572)

antoinelab01 committed 3 years ago

afb43923

feat(group_theory/transfer): Define the transfer homomorphism (#13446)

tb65536 committed 3 years ago

d444a279

Newer Older