leanprover-community/mathlib3

Pull Requests Commits

Fix linting and lemma reference

khwilson committed 3 years ago

744de291

Remove dependence on archimedean in continued fractions

khwilson committed 3 years ago

4efcda94

feat(order/filter/archimedean): Generalize tendsto_coe_nat_at_top_iff to floor_semirings

khwilson committed 3 years ago

3fcd9102

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

feat(set_theory/cardinal): Lift `min` and `max` (#12518)

vihdzp committed 3 years ago

0964573a

feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups (#11744)

nomeata committed 3 years ago

717b11ec

docs(algebra/group/hom): fix typo (#12723)

ericrbg committed 3 years ago

a50de33f

chore(number_theory/primorial): speed up some proofs (#12714)

Ruben-VandeVelde committed 3 years ago

35bb571b

feat(algebraic_geometry/projective_spectrum): basic definitions of projective spectrum (#12635)

jjaassoonn committed 3 years ago

a8bfcfed

feat(data/nat/fib): norm_num plugin for fib (#12463)

kmill committed 3 years ago

a7a2f9d4

feat(data/pnat/find): port over `nat.find` API (#12413)

pechersky committed 3 years ago

500a1d32

feat(group_theory/subsemigroup/basic): subsemigroups (#12111)

pechersky committed 3 years ago

bbc66b5e

chore(measure_theory/function): split files strongly_measurable and simple_func_dense (#12711)

sgouezel committed 3 years ago

50691e59

feat(ring_theory/fractional_ideal): two span_singleton lemmas (#12656)

Multramate committed 3 years ago

ba6c84dd

feat(algebra/group_power/order): add le_pow (#12436)

seangolinski7 committed 3 years ago

17c74f19

feat(topology/bornology/hom): Locally bounded maps (#12046)

YaelDillies committed 3 years ago

91f98e82

feat(set_theory/ordinal_arithmetic): A set of ordinals is bounded above iff it's small (#11870)

vihdzp committed 3 years ago

68033a22

feat(analysis/seminorm): three simple lemmas about balls (#12720)

mcdoll committed 3 years ago

a452bfa1

feat(algebra/parity + data/{int, nat}/parity): parity lemmas for general semirings (#12718)

adomani committed 3 years ago

1f1289fc

chore(scripts): update nolints.txt (#12728)

leanprover-community-bot committed 3 years ago

cbd61731

chore(data/equiv/basic): use `option.elim` and `sum.elim` (#12724)

urkud committed 3 years ago

45061f36

Older