Commits leanprover-community/mathlib

Merge branch 'master' into classical_2

vihdzp committed 3 years ago

e7210f3e

some more

vihdzp committed 3 years ago

b3f278df

feat(topology/algebra/infinite_sum): lemmas about `mul_opposite` (#13674)

eric-wieser committed 3 years ago

df9683ca

refactor(algebra/{group,group_with_zero/basic): Delete lemmas generalized to division monoids (#14042)

YaelDillies committed 3 years ago

3ea573ef

chore({data/{finset,set},order/filter}/pointwise): Reorganize files (#14021)

YaelDillies committed 3 years ago

e6896117

chore(analysis/normed_space/basic): reorder the `restrict_scalars` definitions (#13995)

eric-wieser committed 3 years ago

45d2b523

feat(algebra/module/submodule_bilinear): add `submodule.map₂`, generalizing `submodule.has_mul` (#13709)

eric-wieser committed 3 years ago

91489acb

feat(topology/algebra/group): Division is an open map (#14028)

YaelDillies committed 3 years ago

34f29db3

move(order/synonym): Group `order_dual` and `lex` (#13769)

YaelDillies committed 3 years ago

c8926223

feat(analysis/convex/*): Convexity and subtraction (#14015)

YaelDillies committed 3 years ago

37c691f7

chore(.github/workflows): disable merge conflicts bot for now (#14057)

kim-em committed 3 years ago

56503664

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

leanprover-community-bot committed 3 years ago

153b20f5

fix(data/real/ennreal): style and golfing (#14055)

kbuzzard committed 3 years ago

b17070db

chore(ring_theory/hahn_series): golf a proof (#14054)

urkud committed 3 years ago

87069e91

feat(group_theory/subsemigroup/{center, centralizer}): define center and centralizer as subsemigroups (#13627)

j-loreaux committed 3 years ago

c5e0299a

feat(model_theory/semantics): Realizing restricted terms and formulas (#14014)

awainverse committed 3 years ago

260d5ced

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