leanprover-community/mathlib3

Pull Requests Commits

nomeata committed 3 years ago

c3c6db14

nomeata committed 3 years ago

fe56320f

Use proof by contradiction; fix lemma direction

nomeata committed 3 years ago

3f0f5016

Simplify (simp works under ∃)g

nomeata committed 3 years ago

330bbea4

Simpler calc subproofs

nomeata committed 3 years ago

45e08eed

Use exists_not_mem_of_length_le

nomeata committed 3 years ago

00e4d812

Move other lemmas

nomeata committed 3 years ago

d80f7ad1

feat(set_theory/cardinal): add three_le

nomeata committed 3 years ago

d0597ce3

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

feat(algebra/big_operators/intervals): summation by parts (#11814)

ecstatic-morse committed 3 years ago

98643bca

feat(data/equiv): define `ring_equiv_class` (#11977)

Vierkantor committed 3 years ago

3ca16d0a

chore(algebra/star/self_adjoint): extract a lemma from `has_scalar` (#12121)

eric-wieser committed 3 years ago

223f1496

doc(analysis/normed/group/basic): add docstring explaining the "insert" name (#12100)

eric-wieser committed 3 years ago

aed97e03

Older