Commits leanprover-community/mathlib3

Merge branch 'master' into F_spaces

faenuccio committed 3 years ago

45792550

chore(number_theory/number_field/embeddings): golf (#16804)

alreadydone committed 3 years ago

eaf5cf6b

fix(geometry/euclidean/oriented_angle): correct lemma name (#16821)

jsm28 committed 3 years ago

9cf494e0

feat(counterexamples/zero_divisors_in_add_monoid_algebras + data/finsupp/lex): add a counterexample (#16236)

adomani committed 3 years ago

a87fad7b

feat(ring_theory/derivation): Endomorphisms of the Kähler differential module (#15854)

erdOne committed 3 years ago

28e5032b

feat(algebra/{hom,ring}): extra coercion lemmas for `{mul,add,ring}_equiv` (#16725)

Vierkantor committed 3 years ago

54619e05

feat(algebraic_topology/dold_kan): N₁ reflects isomorphisms (#16778)

joelriou committed 3 years ago

78dddf53

chore(topology/algebra/module/weak_dual): golf `weak_dual.t2_space` (#16816)

ADedecker committed 3 years ago

a4dddb59

feat(algebra/indicator_function): the inverse image under a constant indicator function has four possibilities (#16041)

adomani committed 3 years ago

881d122b

feat(combinatorics/ssyt): add definition and basic API for semistandard Young tableaux (#16195)

jakelev committed 3 years ago

07cdf30b

perf(number_theory/padics/hensel): fix timeout in `calc_eval_z' (#16823)

alreadydone committed 3 years ago

02625770

chore(algebra/category/Group/injective): remove redundant empty line (#16814)

jjaassoonn committed 3 years ago

d1e68751

fix(docs/references.bib): re-introduce authors in Cassels-Frohlich (#16813)

faenuccio committed 3 years ago

224ee5db

feat(topology/sheaves/skyscraper): stalk functor is adjoint to skyscraper functor (#16790)

jjaassoonn committed 3 years ago

fe37df4f

feat(algebra/module/projective): projective modules are closed under product (#16735)

antoinelab01 committed 3 years ago

248bafa2

feat(analysis/inner_product_space/gram_schmidt_ortho): generalize orthonormal basis construction (#16477)

hrmacbeth committed 3 years ago

96055b68

feat(topology/locally_finite): add lemmas about `option _` and `sum _ _` (#15923)

urkud committed 3 years ago

7952bc6d

perf(analysis/calculus/specific_functions): speed up `exp_neg_inv_glue.f_aux_deriv` (#16812)

alreadydone committed 3 years ago

7c0ff89b

feat(set_theory/cardinal/finite): Add `nat.card_fun` (#16799)

tb65536 committed 3 years ago

daa660ca

refactor(ring_theory/roots_of_unity): Remove redundant variables (#16798)

tb65536 committed 3 years ago

83bf40c1

refactor(algebra/group/with_one): `inv_one_class` and related instances (#16697)

jsm28 committed 3 years ago

cb7da1b4

refactor(algebraic_geometry/projective_spectrum/scheme): use homogenous localization API (#16693)

jjaassoonn committed 3 years ago

735ce9d9

feat(geometry/euclidean/oriented_angle): oriented angles between points (#16279)

jsm28 committed 3 years ago

074ba985

feat(measure_theory/covering/density_theorem): add a version of Lebesgue's density theorem (#16762)

ocfnash committed 3 years ago

a17aefd3

feat(algebraic_geometry/morphisms/basic): Morphism properties on the diagonal morphism. (#16111)

erdOne committed 3 years ago

7316286f

feat(topology/algebra/module/weak_dual): add a `t2_space` instance for the `weak_dual` (#16801)

j-loreaux committed 3 years ago

fd4806c1

feat(group_theory/sylow): Technical fusion lemma for Burnside's transfer theorem (#16800)

tb65536 committed 3 years ago

1b2d1a4a

feat(algebra/gcd_monoid/finset): Generalize `finset.gcd_image` (#16795)

YaelDillies committed 3 years ago

0830c456

misc(linear_algebra, ring_theory): more simple facts about `is_simple_module` and order on submodules (#16786)

ADedecker committed 3 years ago

7c1d0d8e

feat(linear_algebra/tensor_product): add variant of ext_fourfold (#16724)

kbuzzard committed 3 years ago

095a77bb