leanprover-community/mathlib

Pull Requests Commits

feat(data/nat/prime): move nat.prime_iff_prime_int; add int.prime_two/three (#12133)

Ruben-VandeVelde committed 3 years ago

afcc7e74

feat(topology/algebra/{group,monoid}): nat and int scalar multiplication is continuous (#12124)

eric-wieser committed 3 years ago

37019db9

feat(analysis/inner_product_space/projection): norm_sq_eq_sum_norm_sq… (#12096)

hparshall committed 3 years ago

72252b3c

feat(order/filter): prod_assoc (#12002)

PatrickMassot committed 3 years ago

271c3237

feat(group_theory/nilpotent): n-ary products of nilpotent group (#11829)

nomeata committed 3 years ago

d8d2f543

chore(topology/constructions): golf a proof (#12174)

urkud committed 3 years ago

e966efc8

chore(category_theory/limits): make fin_category_opposite an instance (#12153)

TwoFX committed 3 years ago

d0fa7a8e

chore(tactic): fix tactic doc tags (#12131)

robertylewis committed 3 years ago

b04851fe

feat(measure_theory/function/lp_space): generalize some `integrable` lemmas to `mem_ℒp` (#11231)

RemyDegenne committed 3 years ago

8b93d3a5

feat(data/real/pointwise): mul distributes over `infi` and `supr` (#12105)

eric-wieser committed 3 years ago

e60e1f22

feat(analysis/seminorm): smul_sup (#12103)

eric-wieser committed 3 years ago

6298a431

feat(topology/continuous_function/bounded): generalize scalar action (#12098)

eric-wieser committed 3 years ago

6ecd7ab8

feat(topology/uniform_space/cauchy): add `cauchy_seq.comp_injective` (#11986)

urkud committed 3 years ago

6ae1b702

feat(ring_theory/witt_vector): assorted facts about Witt vectors over char p rings (#12093)

robertylewis committed 3 years ago

7e1ef9f8

feat(algebra/order/ring): add three_ne_zero and four_ne_zero (#12142)

Ruben-VandeVelde committed 3 years ago

334fb89d

chore(data/nat/factorization): Reorder lemmas and some minor golfing (#12144)

stuart-presnell committed 3 years ago

6c6e142e

chore(data/nat/prime): slightly weaken assumption in nat.exists_prime_and_dvd (#12156)

Ruben-VandeVelde committed 3 years ago

55c9cff7

feat(order/category/FinPartialOrder): The category of finite partial orders (#11997)

YaelDillies committed 3 years ago

fa603fed

feat(analysis/normed_space/star/complex): real and imaginary part of an element of a star module (#11811)

dupuisf committed 3 years ago

56115334

feat(category_theory/isomorphism): two lemmas is_iso.of_iso_comp_left/right on isomorphisms (#12056)

joelriou committed 3 years ago

37775438

feat(algebra/is_prime_pow): dot notation for nat.prime (#12145)

ericrbg committed 3 years ago

bc63071c

doc(group_theory/coset): Mention "Lagrange's theorem" (#12137)

tb65536 committed 3 years ago

628e8fbf

feat(analysis/inner_product_space/pi_L2): Orthonormal basis (#12060)

Daniel-Packer committed 3 years ago

e88badbf

chore(topology/bases): golf a proof (#12127)

urkud committed 3 years ago

518b5d25

feat(algebra/group/pi): add pi.nsmul_apply (#12122)

alexjbest committed 3 years ago

213e2ed7

feat(tactic/swap_var): name juggling, a weaker wlog (#12006)

pechersky committed 3 years ago

b3d09448

fix(category_theory/limits): improve inaccurate docstrings (#12130)

TwoFX committed 3 years ago

5f46dd09

feat(number_theory/divisors): add `prod_div_divisors` and `sum_div_divisors` (#12087)

stuart-presnell committed 3 years ago

7b6c4072

refactor(topology/metric_space/completion): change namespace (#12077)

urkud committed 3 years ago

33179f7e

feat(data/nat/fib): add that `fib` is sum of `nat.choose` along antidiagonal (#12063)

kmill committed 3 years ago

18c3e3f0

Newer Older