Commits leanprover-community/mathlib

feat(number_theory/number_field): add mem_roots_of_unity_of_norm_eq_one (#15143)

xroblot committed 3 years ago

bf783181

feat(topology/sheaves/skyscraper): skyscraper presheaf is a sheaf (#16649)

jjaassoonn committed 3 years ago

7295c811

feat(category_theory/morphism_property): miscellaneous basic results (#16444)

joelriou committed 3 years ago

8150c5eb

feat(algebraic_topology/dold_kan): decomposition of Q (#16357)

joelriou committed 3 years ago

9af20344

feat(algebraic_topology/simplex_category): strong epi mono factorisations (#16276)

joelriou committed 3 years ago

563aed34

feat(*): generalize to and add distrib_smul instances (#16132)

Vierkantor committed 3 years ago

8f78eb9c

chore(number_theory/bernoulli_polynomials): removed unnecessary cast_succ from sum_bernoulli (#16731)

jreaso committed 3 years ago

25c8333e

perf(algebraic_topology/simplicial_object): Speedup `simplicial_cosimplicial_augmented_equiv` (#16729)

YaelDillies committed 3 years ago

2a543b0d

feat(group_theory/schreier): The size of the commutator subgroup is bounded in terms of the index of the center and the number of commutators (#16679)

tb65536 committed 3 years ago

5fefdfa1

refactor(ring_theory/polynomial/tower): review APIs (#16678)

astrainfinita committed 3 years ago

7aebb349

feat(linear_algebra/{basis, determinant, orientation}): determinant of `adjust_to_orientation` of a basis (#16476)

hrmacbeth committed 3 years ago

a753abcf

feat(topology/semicontinuous): characterization by closed sets of semicontinuous maps to a linear order (#16442)

ADedecker committed 3 years ago

c1a28cb2

feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373)

TwoFX committed 3 years ago

e4ee4e30

feat(algebra/module/localized_module): universal property of localized module (#15559)

jjaassoonn committed 3 years ago

aa701d8f

feat(data/polynomial/ring_division): add bUnion_roots_finite (#16670)

xroblot committed 3 years ago

866664b8

feat(analysis/inner_product/orientation, geometry/euclidean/oriented_angle): use bundled orthonormal bases (#16475)

hrmacbeth committed 3 years ago

2fb109f0

refactor(analysis/normed/group/basic): Replace `normed_add_comm_group.core` with group norms (#16238)

YaelDillies committed 3 years ago

73afba48

feat(order/hom/heyting): Heyting homomorphisms (#15308)

YaelDillies committed 3 years ago

98c61b1e

feat(analysis/locally_convex): the topology of a locally convex space is generated by seminorms (#15035)

mcdoll committed 3 years ago

6e5e3f68

feat(algebra/free_monoid): add 2 lemmas (#16712)

urkud committed 3 years ago

be05d53c

feat(algebra/hom/group): `simp` lemmas for applying generic morphism coercions (#16700)

Vierkantor committed 3 years ago

cc967daa

refactor(algebra/order/{smul,module}): Turn lemmas around (#16696)

YaelDillies committed 3 years ago

64ad902d

feat(category_theory/localization): whiskering_left_equivalence and definition of the predicate (#16646)

joelriou committed 3 years ago

a52be2a5

feat(category_theory/groupoid): simplify groupoid.inv to category_theory.inv (#16624)

alreadydone committed 3 years ago

c804ede6

feat(linear_algebra/quadratic_form/basic): algebraic lemmas about `bilin_form.to_quadratic_form` (#16616)

eric-wieser committed 3 years ago

3df3c617

move(algebra/order/ring_lemmas): Rename file (#16520)

YaelDillies committed 3 years ago

98ed2a20

feat(analysis/convex/between): betweenness in affine spaces (#16191)

jsm28 committed 3 years ago

699c2cab

feat(topology/instances/nnreal): generalize `has_continuous_smul` instance (#16713)

j-loreaux committed 3 years ago

b2a65720

feat(data/fin): golf, add lemmas (#16711)

urkud committed 3 years ago

af90fef9

feat(group_theory/quotient_group): `simp` lemmas for `quotient_group.map` (#16703)

Vierkantor committed 3 years ago

d610cec7