Commits leanprover-community/mathlib

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

feat(ring_theory/fractional_ideal): `simp` lemmas for `fractional_ideal.canonical_equiv` (#16702)

Vierkantor committed 3 years ago

001ba509

feat(algebra/hom/equiv): two little `simp` lemmas for `units.map_equiv` (#16701)

Vierkantor committed 3 years ago

acd02bbd

feat(topology/sheaves): presheaf on indiscrete space is sheaf iff value at empty is terminal (#16694)

alreadydone committed 3 years ago

3a0be826

feat(topology/continuous_function/{basic, compact}): add a few missing lemmas (#16714)

j-loreaux committed 3 years ago

9b1e9204

feat(analysis/normed_space/basic): add `norm_algebra_map_nnreal` (#16709)

j-loreaux committed 3 years ago

667f2a62

feat(data/fin): iff on add or sub across last-0 break (#15916)

pechersky committed 3 years ago

07e46bcf

feat(tactic/positivity): Extension for `finset.card` (#16637)

YaelDillies committed 3 years ago

4ed50443