Commits leanprover-community/mathlib

feat(order/category/HeytAlg): The category of Heyting algebras (#16250)

YaelDillies committed 3 years ago

51cbe888

feat(linear_algebra/matrix/charpoly) Generalize Cayley-Hamilton theorem. (#15105)

erdOne committed 3 years ago

46146be0

feat(topology/continuous_on): generalise lemma slightly (#16840)

b-mehta committed 3 years ago

90fab282

chore(data/pfunctor/univariate): remove use of `h_generalize` (#16839)

alexjbest committed 3 years ago

827f0b99

feat(algebra/free_monoid/count): new file (#16829)

urkud committed 3 years ago

706345b3

feat(group_theory/transfer): Homomorphism for Burnside's transfer theorem (#16818)

tb65536 committed 3 years ago

cf43320e

feat(data/list/indexes): add map_with_index_append (#16785)

kbuzzard committed 3 years ago

40e377e5

feat(topology/continuous_function/ideals): construct the Galois correspondence between closed ideals in `C(X, 𝕜)` and open sets in `X` (#16677)

j-loreaux committed 3 years ago

54f74fc8

feat(logic/equiv, topology/homeomorph): split a product at a coordinate (#16210)

alreadydone committed 3 years ago

84066cbf

feat(algebraic_geometry/morphisms/finite_type): Morphisms locally of finite type. (#16124)

erdOne committed 3 years ago

64fc7238

chore(data/rat,data/nat): modularize and reduce imports (#16810)

kim-em committed 3 years ago

68054185

fix(algebra/star/free): speedup (#16851)

sgouezel committed 3 years ago

07c3cf2d

perf(topology/continuous_function/stone_weierstrass): fix timeout (#16844)

alreadydone committed 3 years ago

04e93ae3

feat(algebraic_topology): the Čech nerve of a split epi has an extra degeneracy (#16779)

joelriou committed 3 years ago

c965e54c

feat(topology): Completable field lemmas (#16805)

PatrickMassot committed 3 years ago

e36abd0e

feat(tactic/norm_num): permit disabling the calculation of `/`, `%`, `∣` (#16588)

hrmacbeth committed 3 years ago

9cb7e937

feat(analysis/normed/group/basic): Multiplicative, noncommutative normed groups (#15705)

YaelDillies committed 3 years ago

5b0dd140

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