leanprover-community/mathlib

Pull Requests Commits

feat(set_theory/pgame): Lemmas about order and left/right moves (#13590)

vihdzp committed 3 years ago

0bea7a08

feat(set_theory/game/pgame): Empty instances (#13635)

vihdzp committed 3 years ago

26b2d727

feat(linear_algebra/basic): add a simp lemma for comp_right (#13625)

antoinelab01 committed 3 years ago

94f970a6

doc(analysis/normed_space/basic): Explain how to use non-unital normed algebras (#13605)

eric-wieser committed 3 years ago

b62b5314

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

leanprover-community-bot committed 3 years ago

79ea30ce

doc(measure_theory): add some missing `to_additive` docstrings (#13456)

urkud committed 3 years ago

9923362c

feat(algebra/order/archimedean): Comparing with rationals determines the order (#13602)

YaelDillies committed 3 years ago

976c544c

feat(topology/uniform_space/matrix): Add the uniform_space structure on matrices (#13534)

eric-wieser committed 3 years ago

b98bd418

chore(*): use zero_lt_two/two_ne_zero lemmas more (#13609)

Ruben-VandeVelde committed 3 years ago

45470769

feat(combinatorics/pigeonhole): Pigeons in linear commutative rings (#13308)

YaelDillies committed 3 years ago

9eb3858a

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

Newer Older