leanprover-community/mathlib

Pull Requests Commits

mariainesdff committed 3 years ago

ac1d6c0d

feat(ring_theory/dedekind_domain) : add ideal lemmas

mariainesdff committed 3 years ago

b7e3d151

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

refactor(group_theory/abelianization): Define `commutator` in terms of `general_commutator` (#11949)

tb65536 committed 3 years ago

ffc2bdfb

refactor(ring_theory/fractional_ideal): rename lemmas for dot notation, add coe_pow (#12080)

eric-wieser committed 3 years ago

018c7289

feat(ring_theory/fractional_ideal): add coe_ideal lemmas (#12073)

mariainesdff committed 3 years ago

bcf8a6ed

Older