Commits leanprover-community/mathlib3

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

leanprover-community-bot committed 3 years ago

7b94ffe4

fix(algebra/category/Group/equivalence_Group_AddGroup): fix typo (#16067)

jjaassoonn committed 3 years ago

d928d9b4

feat(analysis/normed/group/basic): construct a normed group from a seminormed group satisfying `∥x∥ = 0 → x = 0` (#16066)

ADedecker committed 3 years ago

c553a824

chore(*): restore `subsingleton` instances and remove hacks (#16046)

alreadydone committed 3 years ago

b95b8c7a

feat(polynomial/field_division): Add `root_set_prod` and clean up lemma statements (#16035)

tb65536 committed 3 years ago

791852eb

feat(data/finset/lattice): 3*2 lemmas about max/min and max'/min' (#15978)

adomani committed 3 years ago

0398787b

lint(scripts/lint-style): style linter for _inst_ occurences (#15977)

jcommelin committed 3 years ago

0a58aefa

refactor(order/game_add): move `game_add` to its own file (#15885)

vihdzp committed 3 years ago

b7f327b8

refactor(information_theory/hamming): Separate Hamming norm and dist definitions. (#15820)

linesthatinterlace committed 3 years ago

1b42ac37

feat(algebra/order/with_zero): Add eq_one_of_mul_eq_one lemmas (#15644)

Multramate committed 3 years ago

0d43cc6d

feat(data/list/basic): add `list.length_filter_le` and `list.length_filter_map_le` (#15369)

madvorak committed 3 years ago

d13cc099

feat(topology/algebra/uniform_ring): ring completions and algebra structures (#14841)

mariainesdff committed 3 years ago

0f4d823c

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