Commits leanprover-community/mathlib

actual_init

awainverse committed 3 years ago

a3cc71c0

init

awainverse committed 3 years ago

8c58d4be

chore(topology/metric_space/hausdorff_distance): move two lemmas (#12771)

hrmacbeth committed 3 years ago

a1bdaddf

feat(algebraic_topology/fundamental_groupoid): Fundamental groupoid of punit (#12757)

prakol16 committed 3 years ago

11b2f36b

feat(group_theory/order_of_element): 1 is finite order, as is g⁻¹ (#12749)

Julian committed 3 years ago

cd196a8a

chore(topology/compact_open): remove `continuous_map.ev`, and rename related lemmas to `eval'` (#12738)

eric-wieser committed 3 years ago

c9c4f40b

feat(group_theory/subgroup/basic): One-sided closure induction lemmas (#12725)

tb65536 committed 3 years ago

a6158f19

feat(number_theory/function_field): the ring of integers of a function field is not a field (#12705)

mariainesdff committed 3 years ago

b1bf390d

feat(group_theory/sylow): direct product of sylow groups if all normal (#11778)

nomeata committed 3 years ago

c3ecf005

feat(model_theory/basic, elementary_maps): Uses `fun_like` approach for first-order maps (#12755)

awainverse committed 3 years ago

31391dc2

feat(algebra/parity + *): generalize lemmas about parity (#12761)

adomani committed 3 years ago

9d7a6645

feat(topology/algebra/const_mul_action): add is_closed smul lemmas (#12747)

mcdoll committed 3 years ago

3ba25ea6

feat(category_theory/abelian/injective_resolution): homotopy between descents of morphism and two injective resolutions (#12743)

jjaassoonn committed 3 years ago

87ab09ca

refactor(analysis/specific_limits): split into two files (#12759)

hrmacbeth committed 3 years ago

7000efb8

refactor(linear_algebra/ray): redefine `same_ray` to allow zero vectors (#12618)

urkud committed 3 years ago

877f2e7a

docs(algebraic_topology/fundamental_groupoid/induced_maps): fix diagram rendering (#12745)

Ruben-VandeVelde committed 3 years ago

e5470580

feat(combinatorics/simple_graph/connectivity): API for get_vert (#12604)

kbuzzard committed 3 years ago

d1e13043

feat(category_theory/punit): A groupoid is equivalent to punit iff it has a unique arrow between any two objects (#12726)

prakol16 committed 3 years ago

192819b4

feat(topology/homotopy/fundamental_group): prove fundamental group is independent of basepoint in path-connected spaces (#12234)

mlavrent committed 3 years ago

3a0532a8

chore(*): move code, golf (#12753)

urkud committed 3 years ago

4d350b97

chore(category_theory/preadditive/projective_resolution): some minor golf (#12739)

jjaassoonn committed 3 years ago

b3abae50

feat(model_theory/basic, terms_and_formulas): Helper functions for constant symbols (#12722)

awainverse committed 3 years ago

b24372f6

feat(group_theory/subgroup/basic): `map_le_map_iff_of_injective` for `subtype` (#12713)

tb65536 committed 3 years ago

3b91c324

feat(algebra/algebra/basic,data/matrix/basic): resolve a TODO about `alg_hom.map_smul_of_tower` (#12684)

eric-wieser committed 3 years ago

c459d2b5

feat(group_theory/quotient_group) finiteness of groups for sequences of homomorphisms (#12660)

Multramate committed 3 years ago

6a71007a

feat(topology/algebra/order/basic): f ≤ᶠ[l] g implies limit of f ≤ limit of g (#12727)

khwilson committed 3 years ago

2e9985e9

feat(number_theory/cyclotomic/basic): add is_primitive_root.adjoin (#12716)

riccardobrasca committed 3 years ago

693a3ac9

feat(data/finset/basic): add finset.filter_eq_self (#12717)

alexjbest committed 3 years ago

b8faf130

feat(category_theory/abelian/injective_resolution): descents of a morphism (#12703)

jjaassoonn committed 3 years ago

d495afdd

feat(measure_theory/function/jacobian): change of variable formula in integrals in higher dimension (#12492)

sgouezel committed 3 years ago

f21a7605