Commits leanprover-community/mathlib

Merge branch 'master' into lax_grothendieck_bicat

kbuzzard committed 3 years ago

1f0f92cf

compiling with norms

kbuzzard committed 3 years ago

f99cd8dc

some fixes

kbuzzard committed 3 years ago

a939e738

Merge branch 'master' into imo1979q1

kbuzzard committed 3 years ago

5c87f5e9

feat(analysis/calculus/cont_diff): `iterated_fderiv[_within]` is linear in the function (#15902)

ADedecker committed 3 years ago

90dc6175

feat(category_theory/limits): has_limits_of_shape J if and only if const J is a left adjoint (#15859)

TwoFX committed 3 years ago

18302a46

chore(tactic/group): do not swallow errors from simp_core (#15835)

eric-wieser committed 3 years ago

ecb66ca5

feat(field_theory/splitting_field): Adjoining all of the roots of a polynomial gives a splitting field (#15795)

tb65536 committed 3 years ago

fae3ce12

refactor(topology/algebra/infinite_sum): generalize `tsum_zero` (#15786)

pechersky committed 3 years ago

adb6142d

feat(ring_theory/dedekind_domain/ideal): the prime factorizations of `r` and `span {r}` are essentially the same in a PID (#15758)

Paul-Lez committed 3 years ago

0672fa47

feat(category_theory/closed/monoidal): transport monoidal_closed across a monoidal equivalence (#15530)

antoinelab01 committed 3 years ago

28959d93

feat(category_theory/products/basic): equivalence ((A ⥤ B) × (A ⥤ C)) ≌ (A ⥤ (B × C)) (#15445)

antoinelab01 committed 3 years ago

3db63953

feat(measure_theory/probability_mass_function): Probability one iff support equals singleton (#15334)

dtumad committed 3 years ago

6375f851

docs(group_theory/p_group): Swap mismatched docstrings (#16065)

tb65536 committed 3 years ago

89f46ddd

feat(data/sign): `sign_one`, `sign_mul`, `sign_pow` (#16058)

jsm28 committed 3 years ago

2230ae61

feat(linear_algebra/ray): relation to linear independence (#16056)

jsm28 committed 3 years ago

9d24857b

feat(category_theory/lifting_properties): adjunctions (#16038)

joelriou committed 3 years ago

24855f46

feat(logic/basic): given two different elements, one of the two is different from a third (#16023)

adomani committed 3 years ago

909cae04

feat(topology/quasi_separated): Define quasi-separated topological spaces. (#15999)

erdOne committed 3 years ago

33261fbe

feat(category_theory): compute subobjects of structured arrows (#15912)

TwoFX committed 3 years ago

3e0dd193

refactor(analysis/normed_space/pi_Lp): make argument of pi_Lp a term of ℝ≥0∞ instead of ℝ (#15833)

j-loreaux committed 3 years ago

e6f3561b

feat(ring_theory/etale): Localization and formally etale homomorphisms. (#15813)

erdOne committed 3 years ago

8a2d93a0

feat(combinatorics/simple_graph): add three useful lemmas relating walk.support and walk.append (#15687)

bottine committed 3 years ago

cdb7af2f

feat(analysis/seminorm): Group seminorms (#15594)

YaelDillies committed 3 years ago

fb1787b1

refactor(analysis/inner_product_space): rename `is_self_adjoint` to `is_symmetric` and add `is_self_adjoint` (#15326)

mcdoll committed 3 years ago

5c91a35b

feat(ring_theory/polynomial/vieta): add version of prod_X_add_C_eq_sum_esymm for multiset (#15008)

xroblot committed 3 years ago

05d8b4f3

feat(topology/uniform_space/uniform_convergence_topology): continuity of [pre,post]composition, and other topological properties (#14534)

ADedecker committed 3 years ago

f1e5c657

feat(algebraic_geometry/*): Preliminary lemmas for #16059 (#16060)

erdOne committed 3 years ago

34b2a989

feat(topology/algebra/uniform_group): add instance `topological_group_is_uniform_of_compact_space` (#16027)

ocfnash committed 3 years ago

531db2ef

feat(algebraic/dold_kan): construction of the functors N₁ and N₂ (#16003)

joelriou committed 3 years ago

07d11baa