leanprover-community/mathlib3

Pull Requests Commits

feat(data/bundle): make arguments to proj and total_space_mk implicit (#14359)

fpvandoorn committed 3 years ago

9b3ea03d

feat(order/liminf_limsup): composition `g ∘ f` is bounded iff `f` is bounded (#14479)

urkud committed 3 years ago

dba797a4

feat(algebra/char_p/basic): add lemma `ring_char.char_ne_zero_of_finite` (#14454)

MichaelStollBayreuth committed 3 years ago

047db399

feat(measure_theory/integral/lebesgue): integral over finite and countable sets (#14447)

urkud committed 3 years ago

df057e32

refactor(combinatorics/simple_graph/basic): rename induced embedding on complete graphs (#14404)

kmill committed 3 years ago

f0216ff2

feat(data/set/finite,order/*): generalize some lemmas from sets to (co)frames (#14394)

urkud committed 3 years ago

0a0a60cc

feat(data/matrix/basic): lemmas about mul_vec and single (#13835)

eric-wieser committed 3 years ago

892f8899

feat(analysis/asymptotics/asymptotics): generalize `is_O.smul` etc (#14487)

urkud committed 3 years ago

f359d55b

feat(algebra/order/group): helper lemma `0 ≤ a + |a|` (#14457)

Jon Eugster committed 3 years ago

4f1c8cf5

feat(topology/vector_bundle): redefine continuous coordinate change (#14462)

fpvandoorn committed 3 years ago

f4fe7907

refactor(topology/metric_space/lipschitz): use `function.End` (#14502)

urkud committed 3 years ago

60371b88

chore(topology/algebra/uniform_field): Wrap in namespace (#14498)

YaelDillies committed 3 years ago

7d713439

feat(analysis/normed_space/star/character_space): compactness of the character space of a normed algebra (#14135)

dupuisf committed 3 years ago

2a0f4743

feat(data/zmod/quotient): More API for `orbit_zpowers_equiv` (#14181)

tb65536 committed 3 years ago

6b183624

chore(data/polynomial/laurent): remove unused case distinction (#14490)

Ruben-VandeVelde committed 3 years ago

bdf3e970

fix(topology/algebra/module/multilinear): initialize simps projections (#14495)

fpvandoorn committed 3 years ago

26a62b0d

feat(algebra/group_power/basic): `a^2 = b^2 ↔ a = b ∨ a = -b` (#14431)

YaelDillies committed 3 years ago

9dc4b8ec

feat(algebra/order/monoid): Missing `has_exists_mul_of_le` instances (#14476)

YaelDillies committed 3 years ago

8e522f85

chore(algebra/lie/quotient): golf some instances (#14480)

eric-wieser committed 3 years ago

e0b2ad8f

feat(algebra/star): star_single, star_update (#14477)

abentkamp committed 3 years ago

806f673f

chore(combinatorics/simple_graph/basic): remove unnecessary lemma (#14468)

kmill committed 3 years ago

3e79ce40

feat(topology/algebra/group): add `continuous_of_continuous_at_one` (#14451)

urkud committed 3 years ago

1eb73395

feat(algebra/algebra/basic): relax typeclass assumptions (#14415)

astrainfinita committed 3 years ago

0f3e083c

feat(data/polynomial/laurent): a Laurent polynomial can be multiplied by a power of `X` to "become" a polynomial (#14106)

adomani committed 3 years ago

346174e9

chore(analysis/asymptotics): golf 2 proofs (#14473)

urkud committed 3 years ago

87fbbd1f

feat(analysis/asymptotics/asymptotics): add `is_O_const_iff` (#14472)

urkud committed 3 years ago

9e9cc57d

feat(order/monotone): prove `nat.exists_strict_mono` etc (#14435)

urkud committed 3 years ago

615babaf

feat(data/set/lattice): add lemmas about unions over natural numbers (#14393)

urkud committed 3 years ago

cafeaa35

feat(data/polynomial/*): `support_binomial` and `support_trinomial` lemmas (#14385)

tb65536 committed 3 years ago

71270485

refactor(group_theory/sylow): Move basic API earlier in the file (#14367)

tb65536 committed 3 years ago

8315ad02

Newer Older