leanprover-community/mathlib3

Pull Requests Commits

adomani committed 3 years ago

7dc25be8

adomani committed 3 years ago

1647ae63

adomani committed 3 years ago

418c0c6d

adomani committed 3 years ago

925cbab8

adomani committed 3 years ago

84746598

adomani committed 3 years ago

045b88fc

general tightening

adomani committed 3 years ago

753b5339

at least one removal and streamline get_sub

adomani committed 3 years ago

76df0bda

explicit arguments

adomani committed 3 years ago

f3440507

join subtractions

adomani committed 3 years ago

4068465c

add support for `nat.pred`

adomani committed 3 years ago

77e2453b

add_tactic_doc and revise doc-module

adomani committed 3 years ago

cc0b571b

adomani committed 3 years ago

dcf95b13

adomani committed 3 years ago

93ffd023

feat(analysis/seminorm): `restrict_scalars` for seminorms (#16401)

ADedecker committed 3 years ago

56e4f0d5

feat(group_theory/subgroup/basic): Centralizer of closure is intersection of centralizers (#16394)

tb65536 committed 3 years ago

13c6c437

feat(analysis/complex/upper_half_plane): Functions bounded at infinity (#15009)

CBirkbeck committed 3 years ago

62119451

feat(data/polynomial/degree/definitions): add `degree_X_sub_C_le` (#16404)

astrainfinita committed 3 years ago

41626f7d

feat(order/interval): Order intervals (#14807)

YaelDillies committed 3 years ago

63014d26

docs(data/polynomial/ring_division, field_theory/splitting_field): update docs (#16406)

astrainfinita committed 3 years ago

9362a5b5

feat(linear_algebra/matrix): A positive definite matrix has a positive determinant (#16376)

abentkamp committed 3 years ago

914d4216

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

leanprover-community-bot committed 3 years ago

18cf2ca3

feat(topology/sheaves/*): sheafification preserves zero morphisms (#16381)

jjaassoonn committed 3 years ago

a0d1a84d

feat(data/fin/basic): eq_succ_of_ne_zero, coe_cast_pred, succ_pred_above_succ (#16294)

joelriou committed 3 years ago

b799b43d

feat(data/nat/parity): add lemmas nat.bit{0|1}_mod_bit0 (#16396)

MichaelStollBayreuth committed 3 years ago

3c227fc0

chore(category_theory/*): Lint (#16366)

YaelDillies committed 3 years ago

3f409bd9

feat(data/finsupp/ne_locus): add a not-member lemma (#16245)

adomani committed 3 years ago

b3b5475d

feat(category_theory/sites/sheaf): category of sheaf is preadditive when target is preadditive (#16324)

jjaassoonn committed 3 years ago

a67ec23d

chore(algebra/order/ring): golf a few proofs (#16398)

urkud committed 3 years ago

fbebf1a0

feat(category_theory/limits/shapes/products): if each `f b ⟶ g b` is mono, then `∏ f ⟶ ∏ g` is mono (#16180)

jjaassoonn committed 3 years ago

e11bafa5

Older