leanprover-community/mathlib3

Pull Requests Commits

attempt to merge master

kim-em committed 4 years ago

92738519

feat(data/support): add `function.mul_support` (#6791)

urkud committed 4 years ago

a0a21774

feat(linear_algebra): composing with a linear equivalence does not change the image (#6816)

TwoFX committed 4 years ago

ffca31af

feat(data/finsupp/basic): add `can_lift (α → M₀) (α →₀ M₀)` (#6777)

urkud committed 4 years ago

e54f6339

feat(algebra/group/type_tags): adding function coercion for `additive` and `multiplicative` (#6657)

ashwiniyengar committed 4 years ago

480b00c8

feat(linear_algebra/dual): add dual_annihilator_sup_eq_inf_dual_annihilator (#6808)

kex-y committed 4 years ago

0b543c34

feat(algebra/subalgebra): missing norm_cast lemmas about operations (#6790)

kim-em committed 4 years ago

f3a4c480

feat(algebra/smul_regular): add `M`-regular elements (#6659)

adomani committed 4 years ago

e7d74ba3

feat(data/finset/basic): add strong_induction and strong_induction_eq (#6682)

agjftucker committed 4 years ago

5be0b0c5

chore(order/filter/bases): a few more constructors (#6798)

urkud committed 4 years ago

3f74b10e

refactor(category_theory/subobject): split into smaller files (#6796)

kim-em committed 4 years ago

852064aa

feat(topology/algebra/continuous_functions): missing lemmas (#6782)

kim-em committed 4 years ago

5d67033c

chore(scripts): update nolints.txt (#6793)

leanprover-community-bot committed 4 years ago

a22df998

feat(analysis/normed_space): normed_algebra.to_topological_algebra (#6779)

kim-em committed 4 years ago

f331648c

feat(ring_theory): define `left_mul_matrix` and `algebra.trace` (#6653)

Vierkantor committed 4 years ago

abfddbf8

feat(data/polynomial): Bernstein polynomials (#6465)

kim-em committed 4 years ago

b75ec5cf

feat(algebra/module/linear_map): Add linear_map.iterate (#6377)

Ruben-VandeVelde committed 4 years ago

4cc42077

feat(topology/continuous_map): formulas for sup and inf in terms of abs (#6720)

kim-em committed 4 years ago

e20c7304

feat(measure_theory/interval_integral): add `integral_comp_mul_left` (#6787)

benjamindavidson committed 4 years ago

31531531

feat(analysis/normed_space/basic): generalize submodule.normed_space (#6766)

eric-wieser committed 4 years ago

240836ae

feat(category_theory/subterminal): subterminal category equiv subobjects of terminal (#6755)

b-mehta committed 4 years ago

d6506747

doc(docs/overview): Update overview (#6772)

tb65536 committed 4 years ago

86b8f39f

feat(combinatorics/quiver): define quivers (#6680)

dwarn committed 4 years ago

5d7efa03

chore(ring_theory/adjoin/basic): golf some proofs about algebra.adjoin (#6784)

eric-wieser committed 4 years ago

df4c9c95

chore(topology/metric_space): add '@[continuity]' attributes (#6780)

kim-em committed 4 years ago

9f77db21

refactor(algebraic_topology/simplex_category): Make simplex_category universe polymorphic. (#6761)

adamtopaz committed 4 years ago

695d7f4f

refactor(category_theory/cones): golf and cleanup cones (#6756)

b-mehta committed 4 years ago

4db82a40

feat(category_theory/closed): currying rfl lemmas (#6754)

b-mehta committed 4 years ago

56e5aa74

fix(analysis/special_functions/integrals): move lemmas out of namespace (#6778)

benjamindavidson committed 4 years ago

b0150a5d

feat(topology): continuous_pi_iff pi.has_continuous_mul pi.topological_group (#6689)

agjftucker committed 4 years ago

26fcfbc9

Older