Commits leanprover-community/mathlib3

feat(data/matrix/basic): dependently-typed block diagonal (#7068)

eric-wieser committed 4 years ago

c3c7c349

feat(continuous_function/compact): lemmas characterising norm and dist (#7054)

kim-em committed 4 years ago

8459d0a6

feat(algebra/category/Module): free module functor is lax monoidal (#6906)

kim-em committed 4 years ago

919b4e38

feat(category/subobject): complete_lattice instance (#6809)

kim-em committed 4 years ago

893173d6

refactor(topology/algebra/normed_group): generalize to semi_normed_group (#7066)

riccardobrasca committed 4 years ago

9157b577

feat(field_theory/minpoly): remove `is_integral` requirement from `unique'` (#7064)

ericrbg committed 4 years ago

d89bfc41

chore(linear_algebra/basic): add linear_map.one_eq_id (#7063)

eric-wieser committed 4 years ago

36649f8b

chore(logic/basic): generalize eq_iff_true_of_subsingleton to Sort (#7061)

eric-wieser committed 4 years ago

104fb22c

feat(logic/function/basic): add injectivity/surjectivity of functions from/to subsingletons (#7060)

adomani committed 4 years ago

b8414e78

feat(data/int/basic algebra/associated): is_unit (a : ℤ) iff a = ±1 (#7058)

adomani committed 4 years ago

df8ef379

feat(archive/imo): formalize IMO 2008 Q4 (#7039)

manuelcandales committed 4 years ago

a6024f10

feat(to_additive): copy _refl_lemma attribute (#7011)

fpvandoorn committed 4 years ago

7e71849c

feat(analysis/special_functions/polynomial): polynomials are big O of polynomials of higher degree (#6714)

dtumad committed 4 years ago

c488997d

feat(big_operators): single out one term from prod (#7040)

PatrickMassot committed 4 years ago

05c491cd

feat(data/*set): some finite sets lemmas (#7037)

PatrickMassot committed 4 years ago

ec6f5d16

feat(tactic/monotonicity): Allow `@[mono]` on `strict_mono` lemmas (#7017)

eric-wieser committed 4 years ago

6048b6f3

feat(ring_theory/hahn_series): summable families of Hahn series (#6997)

awainverse committed 4 years ago

21a96ef0

feat(category_theory/types): add explicit pullbacks in `Type u` (#6973)

gnprice committed 4 years ago

6161a1fb

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

leanprover-community-bot committed 4 years ago

77e90da3

chore(algebra/ring/prod): add missing `prod.distrib` instance (#7069)

eric-wieser committed 4 years ago

d904c8d2

chore(group_theory/specific_groups/*): new folder specific_groups (#7018)

Julian-Kuelshammer committed 4 years ago

8b33d740

feat(measure_theory/interval_integral): make integral_comp lemmas computable by simp (#7010)

benjamindavidson committed 4 years ago

758d3228

chore(logic/function/basic): remove classical decidable instance from a lemma statement (#6488)

eric-wieser committed 4 years ago

97832daf

feat(data/finsum): sums over sets and types with no finiteness hypotheses (#6355)

kbuzzard committed 4 years ago

a1057a3b

feat(linear_algebra/eigenspace): generalized eigenvalues are just eigenvalues (#7059)

ocfnash committed 4 years ago

6ea4e9b1

feat(data/basic/lean): add lemmas finset.subset_iff_inter_eq_{left, right} (#7053)

adomani committed 4 years ago

9b4f0cf8

doc(undergrad.yaml): add equiv.perm.trunc_swap_factors (#7021)

eric-wieser committed 4 years ago

6a9bf98b

feat(group_theory/perm/cycles): Applying cycle_of to an is_cycle (#7000)

tb65536 committed 4 years ago

aa5ec528

feat(linear_algebra/free_module): a set of linearly independent vectors over a ring S is also linearly independent over a subring R of S (#6993)

adomani committed 4 years ago

ae6d77ba

feat(algebra/group/conj): `is_conj` for `monoid`s, `is_conj.setoid`, and `conj_classes` (#6896)

awainverse committed 4 years ago

5f0dbf65