leanprover-community/mathlib

Pull Requests Commits

refactor(topology/metric_space/lipschitz): generalize to pseudo_emetric_space (#6831)

riccardobrasca committed 4 years ago

78034350

feat(category_theory/subobject): API for working with inequalities (#6818)

TwoFX committed 4 years ago

489f5225

feat(data/fintype/basic): add decidable_mem_range_fintype (#6817)

eric-wieser committed 4 years ago

736b1e81

feat(group_theory/subgroup): add {monoid,add_monoid,ring}_hom.lift_of_right_inverse (#6814)

eric-wieser committed 4 years ago

c2e9ec02

chore(algebra/group/basic): dedup, add a lemma (#6810)

urkud committed 4 years ago

5cafdfff

feat(ring_theory/polynomial/homogenous): add a `direct_sum.gcomm_monoid` instance (#6825)

eric-wieser committed 4 years ago

94f59d8b

refactor(tactic/ring): split off `ring_nf` tactic (#6792)

digama0 committed 4 years ago

9f56a0bf

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

Newer Older