Commits leanprover-community/mathlib3

try a more flexible definition of

eric-wieser committed 4 years ago

f623d7d8

feat(topology/tietze_extension): Tietze extension theorem (#10701)

urkud committed 4 years ago

af683b11

refactor(ring_theory/derivation): use weaker TC assumptions (#10952)

urkud committed 4 years ago

fc66d88c

feat(linear_algebra/quadratic_form/complex): all non-degenerate quadratic forms over ℂ are equivalent (#10951)

eric-wieser committed 4 years ago

55f575f1

feat(data/nat/prime): `prime.dvd_prod_iff`; golf `mem_list_primes_of_dvd_prod` (#10624)

stuart-presnell committed 4 years ago

b434a0db

chore(group_theory/quotient_group): make pow definitionally equal (#10833)

eric-wieser committed 4 years ago

ca554bee

feat(data/finsupp/basic): add lemma `disjoint_prod_add` (#10799)

stuart-presnell committed 4 years ago

cea1988f

feat(data/mv_polynomial): add `mv_polynomial.linear_map_ext` (#10945)

urkud committed 4 years ago

4aa7ac67

chore(data/nat/digits): Eliminate `finish` (#10947)

stuart-presnell committed 4 years ago

8dafccc1

feat(algebra/module/submodule_lattice, linear_algebra/projection): two lemmas about `is_compl` (#10709)

ADedecker committed 4 years ago

7e48e350

refactor(linear_algebra/sesquilinear_form): Use similar definition as used in `bilinear_map` (#10443)

mcdoll committed 4 years ago

a6b2f94a

feat(order/galois_connection, linear_algebra/basic): `x ∈ R ∙ y` is a transitive relation (#10943)

ADedecker committed 4 years ago

d5653736

feat(order/monovary): Monovariance of a pair of functions. (#10890)

YaelDillies committed 4 years ago

2ceda785

chore(combinatorics/simple_graph/basic): Golf and cleanup (#10942)

YaelDillies committed 4 years ago

d145e8e3

feat(analysis/special_functions/non_integrable): examples of non-integrable functions (#10788)

urkud committed 4 years ago

5ac4cd35

feat(algebra/algebra/subalgebra): define the center of a (unital) algebra (#10910)

ocfnash committed 4 years ago

c88943fa

chore(data/finset/prod): eliminate `finish` (#10904)

stuart-presnell committed 4 years ago

3b6bd997

feat(topology/[path_]connected): add random [path-]connectedness lemmas (#10932)

ADedecker committed 4 years ago

ed250f7b

feat(ring_theory/integral_closure): Supremum of integral subalgebras (#10935)

tb65536 committed 4 years ago

7555ea78

refactor(algebra/category/CommRing/constructions): Squeeze a slow simp (#10934)

tb65536 committed 4 years ago

5dd0edef

feat(group_theory/index): relindex_eq_zero_of_le_right (#10928)

tb65536 committed 4 years ago

082665e8

chore(*): ensure all open_locales work without any open namespaces (#10913)

alexjbest committed 4 years ago

d910e835

feat(*) : added missing lemma for pointwise smul of submonoid, add_subgroup, add_submonoid, subsemiring, and semiring. (#10908)

jjaassoonn committed 4 years ago

d14ac1fe

refactor(combinatorics/configuration): Implicit arguments for `nondegenerate.eq_or_eq` (#10885)

tb65536 committed 4 years ago

c2debc48

feat(tactic/observe): have a claim proved by library_search under the hood (#10878)

jcommelin committed 4 years ago

b9fbef82

feat(topology/sober): Specialization & generic points & sober spaces (#10914)

erdOne committed 4 years ago

ab654e5c

feat(category_theory/glue_data): Some more API for glue_data (#10881)

erdOne committed 4 years ago

e473898e

feat(algebraic_geometry/locally_ringed_space): LocallyRingedSpace is cocomplete. (#10791)

erdOne committed 4 years ago

6cfc8d82

feat(group_theory/coset): Embeddings of quotients (#10901)

tb65536 committed 4 years ago

b02e2ea1

feat(analysis/calculus/{f,}deriv): generalize `has_fderiv_at_filter.is_O_sub_rev` (#10897)

urkud committed 4 years ago

b4961da2