leanprover-community/mathlib3

Pull Requests Commits

eric-wieser committed 4 years ago

802ebe4c

Merge remote-tracking branch 'origin/master' into eric-wieser/relax-submodule

eric-wieser committed 4 years ago

4ab08eaf

feat(measure_theory/lp_space): add snorm_norm_rpow (#6619)

RemyDegenne committed 4 years ago

0a16148c

fix(algebra/continued_fractions): fix import (#6677)

kappelmann committed 4 years ago

feab14bc

feat(linear_algebra/alternating): Add dom_coprod (#5269)

eric-wieser committed 4 years ago

b48cf171

feat(topology/algebra/group): Add two easy lemmas (#6669)

PatrickMassot committed 4 years ago

b52337a5

feat(data/nat/fincard): introduce `nat.card`, `enat.card` (#6670)

awainverse committed 4 years ago

464d04af

chore(data/rat/basic): a few trivial lemmas about `rat.denom` (#6667)

urkud committed 4 years ago

70662e1c

feat(topology/basic): `f =ᶠ[𝓝 a] 0` iff `a ∉ closure (support f)` (#6665)

urkud committed 4 years ago

69d71341

feat(data/real/ennreal,topology/*): assorted lemmas (#6663)

urkud committed 4 years ago

c928e34d

refactor(ring_theory/discrete_valuation_ring): `discrete_valuation_ring.add_val` as an `add_valuation` (#6660)

awainverse committed 4 years ago

1e9f6646

feat(measure_theory/bochner_integration): extend the integral_smul lemmas (#6654)

RemyDegenne committed 4 years ago

d61d8bfe

feat(polynomial/algebra_map): aeval_algebra_map_apply (#6649)

mo271 committed 4 years ago

a8af8e88

chore(equiv/*): add missing lemmas to traverse coercion diamonds (#6648)

eric-wieser committed 4 years ago

3e011d66

feat(group_theory/order_of_element): Endomorphisms of cyclic groups (#6645)

tb65536 committed 4 years ago

a3050f42

feat(data/polynomial/eval): prod_comp (#6644)

tb65536 committed 4 years ago

b23e14de

feat(group_theory/solvable): Solvability preserved by short exact sequences (#6632)

tb65536 committed 4 years ago

d5563aea

feat(algebra/algebra/basic): An algebra isomorphism induces a group isomorphism between automorphism groups (#6622)

tb65536 committed 4 years ago

ade8889a

feat(algebra/continued_fractions): add convergence theorem (#6607)

kappelmann committed 4 years ago

552ebeb0

feat(analysis/calculus/tangent_cone): add `unique_diff_on.pi` (#6577)

urkud committed 4 years ago

a7410df0

feat(order/well_founded_set, ring_theory/hahn_series): `hahn_series.add_val` (#6564)

awainverse committed 4 years ago

1b0db8e3

feat(order/filter/cofinite): a growing function has a minimum (#6556)

AlexKontorovich committed 4 years ago

0c26cea2

feat(topology/algebra/nonarchimedean): added nonarchimedean groups and rings (#6551)

ashwiniyengar committed 4 years ago

19ecff8b

feat(group_theory/submonoid/operations): add eq_top_iff' (#6536)

kbuzzard committed 4 years ago

ae33fb09

feat(probability_theory/independence): prove equivalences for indep_set (#6242)

RemyDegenne committed 4 years ago

f4c4d107

feat(algebra/group/defs, data/nat/basic): some `ne` lemmas (#6637)

benjamindavidson committed 4 years ago

c2777528

feat(field_theory/polynomial_galois_group): instances of trivial Galois group (#6634)

tb65536 committed 4 years ago

468b8ffd

feat(field_theory/intermediate_field): coe_pow (#6626)

tb65536 committed 4 years ago

ba6b6899

feat(algebra/group_power/lemmas): add invertible_of_pow_eq_one (#6658)

eric-wieser committed 4 years ago

e6819d3a

fix(tactic/norm_num): perform cleanup even if norm_num fails (#6655)

digama0 committed 4 years ago

ff8c8f58

Older