Commits leanprover-community/mathlib

chore(analysis/locally_convex/balanced_core_hull): relax typeclasses on one lemma

eric-wieser committed 3 years ago

8e329766

refactor(number_theory/legendre_symbol/*): move section `general` from `quadratic_char.lean` into new file `auxiliary.lean` (#14027)

MichaelStollBayreuth committed 3 years ago

98f2779c

feat(model_theory/satisfiability): Definition of categorical theories (#14038)

awainverse committed 3 years ago

31af0e88

feat(model_theory/language_map): Cardinality of languages with constants (#13981)

awainverse committed 3 years ago

5d8b4328

refactor(set_theory/ordinal/arithmetic): Rename theorems to match `nat.log` API (#12733)

vihdzp committed 3 years ago

4eb76a7b

feat(linear_algebra/affine_space/independent): add characterisation of affine independence for modules (#14043)

ocfnash committed 3 years ago

00cec552

chore(analysis/normed_space/basic): add short-circuit instance to obtain module structure over reals (#14013)

ocfnash committed 3 years ago

1fef5154

feat(probability_theory/cond_count): use the counting measure to describe probability in the elementary sense (#13484)

kex-y committed 3 years ago

4da939bf

chore(ring_theory/hahn_series): remove redundant instances (#14045)

ocfnash committed 3 years ago

5397ac0e

feat(category_theory/limits): allow (co)limits over lower universes in algebraic categories (#13990)

kim-em committed 3 years ago

c43486ec

feat(ring_theory/dedekind_domain/adic_valuation): extend valuation (#13462)

mariainesdff committed 3 years ago

ad244dd7

feat(topology/algebra/infinite_sum): summable on subtype iff (#14032)

b-mehta committed 3 years ago

fc640963

feat(order/*): Order constructions under `to_dual`/`of_dual` (#13788)

YaelDillies committed 3 years ago

d55a6545

feat(algebra/order/monoid_lemmas_zero_lt): add some lemmas assuming `has_mul` `has_zero` `preorder` (#13296)

astrainfinita committed 3 years ago

1d9d5739

feat(analysis/special_functions): differentiability of Gamma function (#13000)

loefflerd committed 3 years ago

b38aee47

feat(analysis/normed_space/matrix_exponential): lemmas about the matrix exponential (#13520)

eric-wieser committed 3 years ago

bf8db9b7

rename(imo/imo1972_b2 → imo/imo1972_q5): Fix file name (#14037)

vihdzp committed 3 years ago

77c86ba4

feat(representation_theory/invariants): invariants of `lin_hom` are representation morphisms (#14012)

antoinelab01 committed 3 years ago

8412f1fc

feat(analysis/normed_space/exponential): Generalize `field` lemmas to `division_ring` (#13997)

eric-wieser committed 3 years ago

594ceda9

fix(tactics/alias): Make docstring calculation available to to_additive (#13968)

nomeata committed 3 years ago

afec1d73

chore(algebra/regular/*): generalisation linter (#13955)

ericrbg committed 3 years ago

34b61e3d

feat(algebra/category/Module/basic): `iso.hom_congr`agrees with `linear_equiv.arrow_congr` (#13954)

antoinelab01 committed 3 years ago

52531532

feat(set_theory/pgame/birthday): Birthdays of ordinals (#13714)

vihdzp committed 3 years ago

4f386e66

feat(algebraic_topology/dold_kan): defining some null homotopic maps (#13085)

joelriou committed 3 years ago

1e8f3817

refactor(algebra/{group,group_with_zero/basic): Generalize lemmas to division monoids (#14000)

YaelDillies committed 3 years ago

bf6e13bf

refactor(data/nat/log): Golf + improved theorem names (#14019)

vihdzp committed 3 years ago

449ba97d

feat(topology/algebra/infinite_sum): add `tsum_star` (#13999)

eric-wieser committed 3 years ago

163ef61e

fix(topology/algebra/module/weak_dual): fix namespace issue, add a few extra lemmas (#13407)

dupuisf committed 3 years ago

dd16a836

feat(linear_algebra/linear_pmap): `mk_span_singleton` of the same point (#14029)

YaelDillies committed 3 years ago

69c07a4b

feat(measure_theory/integral): a few more integral lemmas (#14025)

sgouezel committed 3 years ago

6a5d17ee